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

DOI10.1016/S0304-3975(01)00186-4MaRDI QIDQ1606131zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

verificationfirst-order logictimed automatadecidable class

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 3888886 (Why is no real title available?)
• scientific article; zbMATH DE number 1189294 (Why is no real title available?)
• scientific article; zbMATH DE number 3514981 (Why is no real title available?)
• scientific article; zbMATH DE number 1304997 (Why is no real title available?)
• scientific article; zbMATH DE number 1390056 (Why is no real title available?)
• scientific article; zbMATH DE number 1405657 (Why is no real title available?)
• scientific article; zbMATH DE number 1424034 (Why is no real title available?)
• A first order logic for specification of timed algorithms: Basic properties and a decidable class
• A theory of timed automata
• Complexity of deciding Tarski algebra
• On the computational complexity and geometry of the first-order theory of the reals. III: Quantifier elimination
• The benefits of relaxing punctuality

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)