Containment of regular languages in non-regular timing diagram languages is decidable

  • Kathi Fisler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)


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.


Decision Procedure Regular Language Finite Automaton Timing Diagram Algorithmic Verification 
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.


  1. 1.
    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.Google Scholar
  2. 2.
    Bachi Berkane Simona Gandrabur and Eduard Cerny. Timing diagrams: semantics and timing analysis. LASSO Laboratory University of Montreal 1996.Google Scholar
  3. 3.
    J.A. Brzozowski, T. Gahlinger and F. Mavaddat. Consistency and satisfiability of waveform timing specifications. Networks 21:91–107 1991.Google Scholar
  4. 4.
    E. Cerny and K. Khordoc. Interface specifications with conjunctive timing constraints: realizability and compatibility. In Second AMAST Workshop on Real-Time Systems June 1995.Google Scholar
  5. 5.
    Kathryn Fisler. A Unified Approach to Hardware Verification Through a Heterogeneous Logic of Design Diagrams. PhD thesis Indiana University August 1996.Google Scholar
  6. 6.
    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.Google Scholar
  7. 7.
    Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. Journal of the ACM 25(1):116–133 January 1978.Google Scholar
  8. 8.
    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.Google Scholar
  9. 9.
    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.Google Scholar
  10. 10.
    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.Google Scholar
  11. 11.
    Rainer Schlör. A prover for VHDL-based hardware design. In Proc. of Computer Hardware Description Languages and Their Applications August 1995.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Kathi Fisler
    • 1
  1. 1.Department of Computer ScienceRice UniversityHouston

Personalised recommendations