Abstract
Two major difficulties in verification with timed automata are state explosion and dependence of complexity on time constants, even with restricted timing constraints. Based on the observation that a vast majority of timed automata have a very regular timing structure, We propose a class of timed automata, alternating RQ timed automata, andprove that they have simple pathpropertieswhich, even with arbitrary timing constraints, yield efficient verification algorithms. In addition, the complexity of the algorithms is independent of the time constants. Next, we give graphical necessary and sufficient conditions for timed automata to be RQ alternating. Finally, we discuss verification algorithms of alternating RQ L-automata (L-processes).
Supported by Fannie and John Hertz Foundation and SRC under contract 92-DC-008.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algorithms for timing verification base on automata emptiness. IEEE Real-Time Systems Symposium, 1992.
R. Alur, C. Courcoubetis, N. Halbwachs, D. Dill, and H. Wong-Toi. Minimization of timed transition systems. International Conference on Computer-Aided Verification, 1992.
R. Alur, A. Itai, R. Kurshan, and M. Yannakakis. Timing verification by successive approximation. International Conference on Computer-Aided Verification, 1992.
Rajeev Alur and David Dill. Automata for modeling real-time systems. 1990 ACM International Workshop on Timing Issues In the Specification and Synthesis of Digital Systems, 1990.
Felice Balarin and Alberto Sangiovanni-Vincentelli. A verification strategy for timing constrainted systems. International Conference on Computer-Aided Verification, 1992.
E. Clarke, O. Grumberg, and R. Kurshan. A synthesis of two approaches for verifying finite state concurrent systems. Workshop on Automatic Verification Methods for Finite State Systems, 1989.
R.Kurshan E.M.Clarke, I.A.Draghicescu. A unified approach for showing language containment and equivalence between various types of ω-automata. Tech. report, CMU,, 1989.
Z. Har'El and R. Kurshan. Software for analytical development of communications protocols. AT&T Technical Journal, Jan. 1990.
R. Hojati, H. Touati, R. Kurshan, and R. Brayton. Efficient ω-regular languagecontainment. International Conference on Computer-Aided Verification, 1992.
J.E. Hopcroft and J.D. Ullman. Introduction to Automata, Languages and Computation. Addison-Wesley, 1979.
H. Touati, R. Brayton, and R. Kurshan. Testing language containment for ω-automata using bdd's. International workshop on Formal Methods in VLSI Design, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lam, W.K.C., Brayton, R.K. (1993). Alternating RQ timed automata. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_20
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive