Verification for Timed Automata extended with Unbounded Discrete Data Structures

DOI10.2168/LMCS-11(3:20)2015zbMATH Open1448.68314OpenAlexW2763333357MaRDI QIDQ3196352FDOQ3196352

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

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

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)

Cited In (6)

• Real-time verification techniques for untimed systems
• Reachability relations of timed pushdown automata
• Augmenting the discrete timed automaton with other data structures.
• Timed Basic Parallel Processes
• Title not available (Why is that?)
• Complexity bounds for the verification of real-time software

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)