From timed automata to logic — and back

DOI10.1007/3-540-60246-1_158zbMath1193.03069OpenAlexW1772179977MaRDI QIDQ3569043

Carsten Weise, François Laroussinie, Kim Guldstrand Larsen

Publication date: 17 June 2010

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-60246-1_158

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Related Items

Characteristic formulae for fixed-point semantics: a general framework ⋮ Presburger liveness verification of discrete timed automata. ⋮ Adequacy and complete axiomatization for timed modal logic ⋮ Model-checking for real-time systems ⋮ Learning deterministic probabilistic automata from a model checking perspective ⋮ The power of reachability testing for timed automata ⋮ Simulation relations and applications in formal methods ⋮ Composition methods for constructing characteristic formulas for dense-time models ⋮ Generalized discrete timed automata: Decidable approximations for safety verification. ⋮ Pushdown timed automata: A binary reachability characterization and safety verification. ⋮ Timed Control with Observation Based and Stuttering Invariant Strategies ⋮ Alternation-free weighted mu-calculus: decidability and completeness ⋮ Characteristic Formulae for Timed Automata ⋮ Monotonic hybrid systems ⋮ A menagerie of timed automata ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ On decidability of recursive weighted logics ⋮ Non-Interference Control Synthesis for Security Timed Automata ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics