The temporal logic of programs

Keywords

Temporal logic of actions, Temporal logic, Computer science, Linear temporal logic, Interval temporal logic

References

• Intermittent Assertion Proofs in LucidE. A. Ashcroft, William W. Wadge — 1977
• Event Based Reasoning - A System for Proving Correct Termination of ProgramsJesko Schwarz — 1976
• An Introduction to Modal LogicE. J. Lemmon, Dana Scott, Krister Segerberg — 1977
• Proving that computer programs terminate cleanly.Richard L. Sites — 1974
• Formalization of properties of parallel programsE. A. Ashcroft, Zohar Manna — 1970
• Verifying properties of parallel programs: an axiomatic approachSusan Owicki, David Gries — 1976
• Computability and completeness in logics of programs (Preliminary Report)David Harel, Albert R. Meyer, Vaughan Pratt — 1977
• Propositional modal logic of programsMichael J. Fischer, Richard E. Ladner — 1977
• Formal verification of parallel programsRobert Keller — 1976
• Is “sometime” sometimes better than “always”?: Intermittent assertions in proving program correctnessZohar Manna, Richard Waldinger — 1976
• Semantical Analysis of Modal Logic I Normal Modal Propositional CalculiSaul A. Kripke — 1963
• Testing and Generating Infinite Sequences by a Finite AutomatonRobert McNaughton — 1966
• On the theory of programming logicsRobert L. Constable — 1977
• Program Proving as Hand Simulation with a Little InductionR. M. Burstall — 1974
• Proving the Correctness of Multiprocess ProgramsLeslie Lamport — 1977
• Logical Rules of Natural Reasoning about ProgramsFred Kröger — 1976
• Proving Assertions about Parallel ProgramsE. A. Ashcroft — 1975
• An Axiomatic Basis for Computer ProgrammingTony Hoare — 1968
• Procedures and parameters: An axiomatic approachTony Hoare — 1971

Cited by

• On the Expressiveness of TPTL and MTL I,IIPatricia Bouyer, Fabrice Chevalier, Nicolas Markey — 2009
• Matrix Proof Methods for Modal LogicsLincoln Wallen — 1987
• Generating Deterministic ω-Automata for most LTL Formulas by the Breakpoint ConstructionAndreas Morgenstern, Klaus Schneider, Sven Lamberti — 2008
• Verification of concurrent programs, Part I: The temporal frameworkZohar Manna, Amir Pnueli — 1981
• Feature specification and automated conflict detectionAmy Felty, Kedar S. Namjoshi — 2003
• Eigenschaftsorientierte Beschreibung der logischen Architektur eingebetteter SystemeDavid Trachtenherz — 2009
• Monitoring lichens diversity and climatic change in Sierra Nevada (Spain)Marı ́a Rosa Fernández Calzado, Manuel Casares Porcel, Jayne Houston — 2013
• Spécification et vérification des systèmes temps réel réactifs en BMiloud Rached — 2007
• Real-time and Probabilistic Temporal Logics: An OverviewSavas Konur — 2010
• The temporal logic of actionsLeslie Lamport — 1994
• Model checking for input/output properties of a black-box modelWalter Dosch, Pornsiri Muenchaisri, Wuttipong Ruanthong — 2007
• A framework for specifying safe behavior of the CIIP medical system.Seyed Morteza Babamir — 2011
• Formal Verification of Realtime Systems in ASTRALAlberto Coen‐Porisini, Richard A. Kemmerer, Dino Mandrioli — 1993
• Applicability of Process Mining Techniques in Business EnvironmentsAndrea Burattin — 2013
• Towards verifying Petri Nets: a model cheking approachMaría Rosa Martos Salgado — 2010
• Verifying network protocols using temporal logicBrent Hailpern, Susan Owicki — 1980
• Towards a Theory of Trust for the Global Ubiquitous ComputerKarl Krukow, Phd Dissertation, Karl Krukow — 2006
• Keeping fairness aliveMohammad Torabi Dashti — 2008
• Axiomatising the logic of distributed computationSteven G Cumming — 1986
• Time for Action: On the Relation Between Time, Knowledge and ActionYoav Shoham — 1989

Related papers

• Temporal and Dynamic LogicFrank Wolter, Michael Wooldridge — 2010
• Representing RCC relations in temporal logicT. Harteveld — 2015
• Temporal Logic in SpecificationBehnam Banieqbal, Howard Barringer, Amir Pnueli — 1987
• A Linear Temporal Logic with Clocks for Verification of Real-Time SystemsGuangyuan Li — 2002
• Characterizing Kripke structures in temporal logic. Interim reportM. C. Browne, E. M. Clarke, Orna Grümberg — 1987
• The Temporal Description Logic TL-SI and its Decidability AlgorithmKun Hu, Xueli Yu, Zhi Li — 2010
• A Logic for Verifying Metric Temporal Properties in Distributed Hybrid SystemsPing Hou, Yifei Chen — 2018