Abstract
Parametric timing constraints are expressed naturally in timing diagram logics. Algorithmic verification of parametrically constrained timing properties is a difficult problem known to be undecidable in most general cases. This paper establishes that a class of parametrically constrained timing properties can be verified algorithmically against finite-state systems; alternatively stated containment by a regular language is shown decidable for a class of language properties (regular and non-regular) expressible in our timing diagram logic.
This research was conducted while the author was a graduate student at Indiana University with financial support from AT&T Bell Laboratories under the PhD Fellowship Program.
Chapter PDF
References
Rajeev Alur Thomas A. Henzinger and Moshe Y. Vardi. Parametric real-time reasoning. In Proc. of the 25th ACM Symposium on the Theory of Computing pages 592–601 1993.
Bachi Berkane Simona Gandrabur and Eduard Cerny. Timing diagrams: semantics and timing analysis. LASSO Laboratory University of Montreal 1996.
J.A. Brzozowski, T. Gahlinger and F. Mavaddat. Consistency and satisfiability of waveform timing specifications. Networks 21:91–107 1991.
E. Cerny and K. Khordoc. Interface specifications with conjunctive timing constraints: realizability and compatibility. In Second AMAST Workshop on Real-Time Systems June 1995.
Kathryn Fisler. A Unified Approach to Hardware Verification Through a Heterogeneous Logic of Design Diagrams. PhD thesis Indiana University August 1996.
Werner Grass et al. Transformation of timing diagram specifications into VHDL code. In Proc. of Computer Hardware Description Languages and Their Applications pages 659–668 August 1995.
Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. Journal of the ACM 25(1):116–133 January 1978.
Oscar H. Ibarra Tao Jiang Nicholas Tran and Hui Wang. New decidability results concerning two-way counter machines and applications. In Proc. of the 20th International Colloquium on Automata Languages and Programming 1993. Lecture Notes in Computer Science 700.
K. Khordoc M. Dufresne E. Cerny P. A. Babkine and A. Silburt. Integrating behavior and timing in executable specifications. In Proc. of Computer Hardware Description Languages and their Applications pages 385–402 April 1993.
Philippe Mooeschler Hans Peter Amann and Pausto Pellandini. High-level modeling using extended timing diagrams. In Proc. of the European Design Automation Conference pages 494–499 1993.
Rainer Schlör. A prover for VHDL-based hardware design. In Proc. of Computer Hardware Description Languages and Their Applications August 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fisler, K. (1997). Containment of regular languages in non-regular timing diagram languages is decidable. In: Grumberg, O. (eds) Computer Aided Verification. CAV 1997. Lecture Notes in Computer Science, vol 1254. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63166-6_17
Download citation
DOI: https://doi.org/10.1007/3-540-63166-6_17
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63166-8
Online ISBN: 978-3-540-69195-2
eBook Packages: Springer Book Archive