Dynamic linear time temporal logic

DOI10.1016/S0168-0072(98)00039-6zbMath0931.03033OpenAlexW2145394419MaRDI QIDQ1295431

Jesper G. Henriksen, P. S. Thiagarajan

Publication date: 20 July 1999

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(98)00039-6

zbMATH Keywords

expressive completeness\(\omega\)-automatapropositional dynamic logicfinitary axiomatizationDLTLexponential time decision procedurelinear time temporal logicmonadic second-order theory of \(\omega\)-sequences

Mathematics Subject Classification ID

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (19)

Specifying and verifying interaction protocols in a temporal action logic ⋮ Reasoning about actions with Temporal Answer Sets ⋮ On the Model Checking Problem for Some Extension of CTL* ⋮ Tableau-based automata construction for dynamic linear time temporal logic ⋮ Reasoning about actions with \(\mathcal{EL}\) ontologies and temporal answer sets for DLTL ⋮ Propositional Dynamic Logic for Message-Passing Systems ⋮ Business process verification with constraint temporal answer set programming ⋮ Visibly linear temporal logic ⋮ Almost event-rate independent monitoring ⋮ On regular temporal logics with past ⋮ Action and knowledge in alternating-time temporal logic ⋮ Temporal logic with recursion ⋮ Formal Verification for Components and Connectors ⋮ Verifying Agents’ Conformance with Multiparty Protocols ⋮ Expressive Completeness for LTL With Modulo Counting and Group Quantifiers ⋮ A Hierarchical Completeness Proof for Propositional Interval Temporal Logic with Finite Time ⋮ Making Metric Temporal Logic Rational ⋮ Dynamic linear time temporal logic ⋮ On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

Cites Work

• Descriptively complete process logic
• An elementary proof of the completeness of PDL
• Process logic: Expressiveness, decidability, completeness
• Propositional dynamic logic of regular programs
• Dynamic linear time temporal logic
• Reasoning about infinite computations
• Translating regular expressions into small ε-free nondeterministic finite automata
• Testing and generating infinite sequences by a finite automaton
• A product version of dynamic linear time temporal logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Dynamic linear time temporal logic