Linear-time temporal logics with Presburger constraints: an overview ★

DOI10.3166/jancl.16.311-347zbMath1186.03036OpenAlexW2019346963MaRDI QIDQ3647243

Stéphane P. Demri

Publication date: 30 November 2009

Published in: Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.3166/jancl.16.311-347

zbMATH Keywords

computational complexitytemporal logicBüchi automatonPresburger arithmetic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items

An automata-theoretic approach to constraint LTL ⋮ Temporal stream logic modulo theories ⋮ A decidability result for the model checking of infinite-state systems ⋮ ASSUME-GUARANTEE REASONING WITH LOCAL SPECIFICATIONS

Cites Work

• Unnamed Item
• Unnamed Item
• Automata for branching and layered temporal structures. An investigation into regularities of infinite transition systems
• On the interpretability of arithmetic in temporal logic
• Graded modalities. I
• The power of temporal proofs
• From local to global consistency
• A theory of timed automata
• Reasoning about infinite computations
• The complexity of the temporal logic with ``until over general linear time
• Verifying lossy channel systems has nonprimitive recursive complexity.
• Pushdown processes: Games and model-checking
• Equality and monodic first-order temporal logic
• Presburger liveness verification of discrete timed automata.
• Future temporal logic needs infinitely many modalities
• Guest editorial: Temporal representation and reasoning
• LTL over integer periodicity constraints
• Semigroups, Presburger formulas, and languages
• In so many possible worlds
• The complexity of propositional linear temporal logics
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• Datalog with integer periodicity constraints
• Flat fragments of CTL and CTL: separating the expressive and distinguishing powers
• A really temporal logic
• The benefits of relaxing punctuality
• About the decision of reachability for register machines
• Propositional temporal logics: decidability and completeness
• Modal Logics Between Propositional and First-order
• Counting Objects
• NEXP TIME-complete description logics with concrete domains
• Introduction to constraint databases