scientific article

Lenore D. Zuck, Orna Lichtenstein, Amir Pnueli

Publication date: 1985

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

liveness safety normal form semantics temporal logic syntax decision procedure past operators star-free expressions since extreme-fairness infinite- state programs previous sound and complete deductive system

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items

CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus, Verification of multiprocess probabilistic protocols, A branching time logic with past operators, A propositional dense time logic, The logic of ``initially and ``next: complete axiomatization and complexity, Safety, liveness and fairness in temporal logic, Temporal Logic and Fair Discrete Systems, Functional Specification of Hardware via Temporal Logic, Decidability and incompleteness results for first-order temporal logics of linear time, Multi-Valued Reasoning about Reactive Systems, Recognizing safety and liveness, Algorithms for monitoring real-time properties, MetateM: An introduction, A transformation-based synthesis of temporal specification, Decentralised LTL monitoring, Bounded model checking of ETL cooperating with finite and looping automata connectives, Finite-trace linear temporal logic: coinductive completeness, An application of temporal projection to interleaving concurrency, Problems concerning fairness and temporal logic for conflict-free Petri nets, SMT-based satisfiability of first-order LTL with event freezing functions and metric operators, A Cookbook for Temporal Conceptual Data Modelling with Description Logics, Verification in continuous time by discrete reasoning, From linear temporal logics to Büchi automata: the early and simple principle, A survey on temporal logics for specifying and verifying real-time systems, Modelling mutual exclusion in a process algebra with time-outs, An infinitary encoding of temporal equilibrium logic, Bridging the gap between single- and multi-model predictive runtime verification, A simple rewrite system for the normalization of linear temporal logic, A first-order logic characterization of safety and co-safety languages, Finite-trace and generalized-reactivity specifications in temporal synthesis, A first-order logic characterisation of safety and co-safety languages, \textit{Once} and \textit{for all}, Branching versus linear logics yet again, Unnamed Item, LTL is closed under topological closure, Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited, Completing the temporal picture, Control machines: A new model of parallelism for compositional specifications and their effective compilation, Runtime verification of embedded real-time systems, Interval logics and their decision procedures. I: An interval logic, A hierarchy of temporal logics with past, GPU schedulers: how fair is fair enough?, On using temporal logic for refinement and compositional verification of concurrent systems, A model checker for linear time temporal logic, Guest editors' preface to special issue on interval temporal logics, Compositional reasoning using intervals and time reversal, An Automata-Theoretic Approach to Infinite-State Systems, On the Krohn-Rhodes Cascaded Decomposition Theorem, On Decidability of LTL+Past Model Checking for Process Rewrite Systems, On the expressiveness of TPTL and MTL, On regular temporal logics with past, Proving the Refuted: Symbolic Model Checkers as Proof Generators, From Philosophical to Industrial Logics, Unnamed Item, Model-based safety assessment of a triple modular generator with xSAP, Model checking with strong fairness, One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\), Axioms for real-time logics, Monitoring Metric First-Order Temporal Properties, Checking Temporal Properties of Discrete, Timed and Continuous Behaviors, From Monadic Logic to PSL, Characterization of temporal property classes, Modelling knowledge and action in distributed systems, Unnamed Item, Tool support for learning Büchi automata and linear temporal logic, Weak Kripke Structures and LTL, Model-checking Timed Temporal Logics, Alternating automata: Unifying truth and validity checking for temporal logics, Past is for Free: on the Complexity of Verifying Linear Temporal Properties with Past, An axiomatization of PCTL*, A logic-based approach to incremental reasoning on multi-agent systems, Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time, \(\mathsf{GR}(1)\) is equivalent to \(\mathsf{R}(1)\), A two-level temporal logic for evolving specifications., Specification in CTL + past for verification in CTL., Self-stabilizing extensions for message-passing systems, Temporal Logics of Knowledge and their Applications in Security, On the strength of temporal proofs, An experience in proving regular networks of processes by modular model checking, Back to the future: a fresh look at linear temporal logic