Configurable verification of timed automata with discrete variables

DOI10.1007/S00236-020-00393-4MaRDI QIDQ2120808zbMATH OpenOpenAlexFDO

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

Publication date 1 April 2022

Published in Acta Informatica (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s00236-020-00393-4

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 with Discrete Variables
• SAT-based reachability checking for timed automata with discrete data
• Verified model checking of timed automata
• scientific article; zbMATH DE number 1773082
• scientific article; zbMATH DE number 1507209

Cites work

• scientific article; zbMATH DE number 1337733 (Why is no real title available?)
• scientific article; zbMATH DE number 1956585 (Why is no real title available?)
• scientific article; zbMATH DE number 1962849 (Why is no real title available?)
• scientific article; zbMATH DE number 5228180 (Why is no real title available?)
• 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
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Formal Modeling and Analysis of Timed Systems
• Horn clauses for communicating timed systems
• Interpolation and SAT-based model checking.
• Lazy Reachability Checking for Timed Automata with Discrete Variables
• Lazy abstraction
• Lazy reachability checking for timed automata using interpolants
• Lectures on Concurrency and Petri Nets
• Reachability in timed automata with diagonal constraints
• SAT-Based Model Checking without Unrolling
• SMT-based induction methods for timed systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Using non-convex approximations for efficient analysis of timed automata

Cited in

(2)

• Verification for Timed Automata extended with Unbounded Discrete Data Structures
• Lazy Reachability Checking for Timed Automata with Discrete Variables

This page was built for publication: Configurable verification of timed automata with discrete variables

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