Lazy Reachability Checking for Timed Automata with Discrete Variables

DOI10.1007/978-3-319-94111-0_14MaRDI QIDQ5883582zbMATH OpenOpenAlexFDO

Authors Tamás Tóth, István Majzik

Publication date 21 March 2023

Published in Model Checking Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-94111-0_14

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Lazy reachability checking for timed automata using interpolants
• SAT-based reachability checking for timed automata with discrete data
• Configurable verification of timed automata with discrete variables
• Let's be lazy, we have time -- or, lazy reachability analysis for timed automata
• Timed automata relaxation for reachability
• scientific article; zbMATH DE number 5024617
• scientific article; zbMATH DE number 7297846
• Efficient timed model checking for discrete-time systems
• scientific article; zbMATH DE number 2064232

Cites work

• A theory of timed automata
• Automatic Abstraction Refinement for Timed Automata
• Better abstractions for timed automata
• Counterexample-guided abstraction refinement for symbolic model checking
• Difference bound constraint abstraction for timed automata reachability checking
• Horn clauses for communicating timed systems
• scientific article; zbMATH DE number 1956585 (Why is no real title available?)
• Lazy abstraction
• Lazy reachability checking for timed automata using interpolants
• SMT-based induction methods for timed systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Using non-convex approximations for efficient analysis of timed automata

Cited in

(4)

• Let's be lazy, we have time -- or, lazy reachability analysis for timed automata
• Lazy reachability checking for timed automata using interpolants
• Configurable verification of timed automata with discrete variables
• Efficient strategies for CEGAR-based model checking

This page was built for publication: Lazy Reachability Checking for Timed Automata with Discrete Variables

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