Decidable verification for reducible timed automata specified in a first order logic with time

DOI10.1016/S0304-3975(01)00186-4zbMATH Open1026.68079OpenAlexW1975997547MaRDI QIDQ1606131FDOQ1606131

Authors: Danièle Beauquier, Anatol Slissenko 

Publication date: 31 July 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(01)00186-4

Recommendations

• Publication:4934321
• Verification of timed automata via satisfiability checking
• A first order logic for specification of timed algorithms: Basic properties and a decidable class
• Verified certification of reachability checking for timed automata
• Verified model checking of timed automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Decidability and incompleteness results for first-order temporal logics of linear time
• scientific article; zbMATH DE number 1361136
• Publication:4508304
• Theoretical Aspects of Computing - ICTAC 2004

zbMATH Keywords

verificationfirst-order logictimed automatadecidable class

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Classical first-order logic (03B10)

Cites Work

• A theory of timed automata
• The benefits of relaxing punctuality
• Title not available (Why is that?)
• On the computational complexity and geometry of the first-order theory of the reals. III: Quantifier elimination
• Title not available (Why is that?)
• Complexity of deciding Tarski algebra
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A first order logic for specification of timed algorithms: Basic properties and a decidable class
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (5)

• Decidable properties for monadic abstract state machines
• Decidable Fragments of Many-Sorted Logic
• Decidable fragments of many-sorted logic
• Periodicity based decidable classes in a first order timed logic
• A first order logic for specification of timed algorithms: Basic properties and a decidable class

This page was built for publication: Decidable verification for reducible timed automata specified in a first order logic with time

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1606131)