A survey on temporal logics for specifying and verifying real-time systems

DOI10.1007/s11704-013-2195-2zbMath1425.68258OpenAlexW2110062879MaRDI QIDQ2418645

Savas Konur

Publication date: 28 May 2019

Published in: Frontiers of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11704-013-2195-2

zbMATH Keywords

decidabilitymodel checkingexpressivenessinterval temporal logicsreal-time temporal logicsbranching temporal logicspropositional temporal logicsprobabilistic temporal logicsfirst-order linear temporal logics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (3)

Spiking neural P systems: matrix representation and formal verification ⋮ Search-based testing in membrane computing ⋮ A conceptual framework for resilience: fundamental definitions, strategies and metrics

Uses Software

• Isabelle
• Kronos
• Uppaal
• DCVALID
• IDLVALID
• ICS
• Modechart

Cites Work

• Maintaining knowledge about temporal intervals
• A logic-based calculus of events
• On the completeness and decidability of duration calculus with iteration
• Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions
• The complexity of temporal logic over the reals
• A hierarchy of temporal logics with past
• A critical examination of Allen's theory of action and time
• Quantitative temporal logics over the reals: PSpace and below
• An optimal decision procedure for right propositional neighborhood logic
• Using branching time temporal logic to synthesize synchronization skeletons
• Towards a general theory of action and time
• The power of temporal proofs
• Probabilistic duration calculus for continuous time
• Polytime model checking for times probabilistic computation tree logic
• Non-elementary lower bound for Propositional Duration Calculus
• Intervals and tenses
• Axioms for tense logic. II: Time periods
• Process logic: Expressiveness, decidability, completeness
• A calculus of durations
• The logic of time. A model-theoretic investigation into the varieties of temporal ontology and temporal discourse.
• Interval semantics for tense logic: Some remarks
• Modal languages and bounded fragments of predicate logic
• Proving properties of states in the situation calculus
• Isabelle. A generic theorem prover
• A logic for reasoning about time and reliability
• Multi-dimensional modal logic
• The complexity of the temporal logic with ``until over general linear time
• Many-dimensional modal logics: theory and applications
• Duration calculus. A formal approach to real-time systems.
• Decidable fragments of first-order temporal logics
• Automatic verification of real-time systems with discrete probability distributions.
• The logic of time. A model-theoretic investigation into the varieties of temporal ontology and temporal discourse
• Axiomatizing the monodic fragment of first-order temporal logic
• A partial order approach to branching time logic model checking.
• Specification in CTL + past for verification in CTL.
• Equality and monodic first-order temporal logic
• A tableau decision algorithm for modalized \(\mathcal A\mathcal L\mathcal C\) with constant domains
• Temporal logic. From ancient ideas to artificial intelligence
• A propositional dynamic logic with qualitative probabilities
• Temporal prepositions and their logic
• Axiomatising first-order temporal logic: Until and since over linear time
• An axiomatization of PCTL*
• Probabilistic temporal logics via the modal mu-calculus
• Reasoning about actions in dynamic linear time temporal logic
• An axiomatization of full Computation Tree Logic
• Interval Duration Logic
• Model checking of probabilistic and nondeterministic systems
• Monodic Fragments of First-Order Temporal Logics: 2000–2001 A.D.
• Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability
• Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems
• Tableaux for Logics of Subinterval Structures over Dense Orderings
• On Expressiveness and Complexity in Real-Time Model Checking
• Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T
• Some Recent Results in Metric Temporal Logic
• Counting CTL
• An Optimal Tableau-Based Decision Algorithm for Propositional Neighborhood Logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• A decidable propositional dynamic logic with explicit probabilities
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• A Modal Logic for Chopping Intervals
• Relations Among Complexity Measures
• The Complexity of Tree Automata and Logics of Programs
• Representing action and change by logic programs
• Decidability and incompleteness results for first-order temporal logics of linear time
• Reasoning about knowledge and probability
• A really temporal logic
• A propositional modal logic of time intervals
• Actions and Events in Interval Temporal Logic
• The benefits of relaxing punctuality
• A probabilistic extension of intuitionistic logic
• Propositional temporal logics: decidability and completeness
• Completeness of neighbourhood logic
• A mixed decision method for duration calculus
• Undecidability of compass logic
• On the Restraining Power of Guards
• Automated Reasoning with Analytic Tableaux and Related Methods
• Alternating timed automata
• CONCUR 2004 - Concurrency Theory
• Take It NP-Easy: Bounded Model Construction for Duration Calculus
• On Decidability and Expressiveness of Propositional Interval Neighborhood Logics
• The Complexity of CTL* + Linear Past
• Discrete Linear-time Probabilistic Logics: Completeness, Decidability and Complexity
• Automated Reasoning with Analytic Tableaux and Related Methods
• Decidable and Undecidable Fragments of Halpern and Shoham’s Interval Temporal Logic: Towards a Complete Classification
• Tools and Algorithms for the Construction and Analysis of Systems
• Theoretical Aspects of Computing - ICTAC 2004
• Clausal temporal resolution
• Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Deciding an Interval Logic with Accumulated Durations
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Formal Modeling and Analysis of Timed Systems
• Computer Aided Verification
• A Road Map of Interval Temporal Logics and Duration Calculi
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A survey on temporal logics for specifying and verifying real-time systems