Verification for Timed Automata extended with Unbounded Discrete Data Structures

DOI10.2168/LMCS-11(3:20)2015MaRDI QIDQ3196352zbMATH OpenOpenAlexFDO

Authors Karin Quaas

Publication date 29 October 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/lmcs-11(3:20)2015

zbMATH Keywords

metric temporal logicpushdown automatareal-time systemstimed automatacounter systems

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Verification for timed automata extended with unbounded discrete data structures
• Reachability results for timed automata with unbounded data structures
• scientific article; zbMATH DE number 1953031
• Verification of timed automata via satisfiability checking
• Configurable verification of timed automata with discrete variables
• SAT-based unbounded model checking of timed automata
• Verified certification of reachability checking for timed automata
• Verified model checking of timed automata
• SAT-based reachability checking for timed automata with discrete data

Cited in

(11)

• Complexity bounds for the verification of real-time software
• Real-time verification techniques for untimed systems
• Automatic verification of multi-queue discrete timed automata
• Reachability relations of timed pushdown automata
• Augmenting the discrete timed automaton with other data structures.
• Reachability results for timed automata with unbounded data structures
• Verification for timed automata extended with unbounded discrete data structures
• Timed bounded verification of inclusion based on timed bounded discretized language
• Hybrid Systems: Computation and Control
• Timed Basic Parallel Processes
• scientific article; zbMATH DE number 1773082 (Why is no real title available?)

This page was built for publication: Verification for Timed Automata extended with Unbounded Discrete Data Structures

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