Abstract
Theoretical investigations of infinite-state systems have so far concentrated on decidability results; in the case of timed automata these results are based on region graphs. We investigate the specific procedure that is used practically in order to decide verification problems, namely symbolic forward analysis. This procedure is possibly nonterminating. We present basic concepts and properties that are useful for reasoning about sufficient termination conditions, and then derive some conditions. The central notions here are constraint transformers associated with sequences of automaton edges and zone trees labeled with successor constraints. © Springer-Verlag Berlin Heidelberg 1999.
Cite
CITATION STYLE
Mukhopadhyay, S., & Podelski, A. (1999). Beyond region graphs: Symbolic forward analysis of timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1738, pp. 232–244). Springer Verlag. https://doi.org/10.1007/3-540-46691-6_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
