Parametric real-time reasoning

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Parametric real-time reasoning

Full text

Pdf (1.05 MB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the twenty-fifth annual ACM symposium on Theory of computing table of contents

San Diego, California, United States

Pages: 592 - 601

Year of Publication: 1993

ISBN:0-89791-591-7

Authors

Rajeev Alur
Thomas A. Henzinger
Moshe Y. Vardi

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 27, Citation Count: 22

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/167088.167242 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Martín Abadi , Leslie Lamport, An Old-Fashioned Recipe for Real Time, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.1-27, June 03-07, 1991
	2	Rajeev Alur, Techniques for automatic verification of real-time systems, Stanford University, Stanford, CA, 1992
	3	R. Alur, C. Courcoubetis, and D. Dill. Modelchecking for real-time systems. In Proc. 5th 1EEE LICS, 1990.
	4	Rajeev Alur , Costas Courcoubetis , Thomas A. Henzinger , Pei-Hsin Ho, Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, Hybrid Systems, p.209-229, January 1993
	5	Rajeev Alur , D. L. Dill, Automata for modeling real-time systems, Proceedings of the seventeenth international colloquium on Automata, languages and programming, p.322-335, July 1990, Warwick University, England
	6	Rajeev Alur , Tomás Feder , Thomas A. Henzinger, The benefits of relaxing punctuality, Proceedings of the tenth annual ACM symposium on Principles of distributed computing, p.139-152, August 19-21, 1991, Montreal, Quebec, Canada [doi>10.1145/112600.112613]
	7	R. Alur and T. Henzinger. A really temporal logic. In Proc. 30th 1EEE FOCS, 1989.
	8	R. Alur and T. Henzinger. Real-time logics: Complexity and expressiveness. In Proc. 5th 1EEE LICS, 1990.
	9	R. Ahr and T. Henzinger. Back to the future: Towards a theory of timed regular languages. In Proc. 33rd IEEE FOCS, 1992.
	10	Hagit Attiya , Cynthia Dwork , Nancy Lynch , Larry Stockmeyer, Bounds on the time to reach agreement in the presence of timing uncertainty, Proceedings of the twenty-third annual ACM symposium on Theory of computing, p.359-369, May 05-08, 1991, New Orleans, Louisiana, United States [doi>10.1145/103418.103457]
	11	Costas Courcoubetis, Minimum and Maximum Delay Problems in Real-Time Systems, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.399-409, July 01-04, 1991
	12	David L. Dill, Timing Assumptions and Verification of Finite-State Concurrent Systems, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, p.197-212, June 12-14, 1989
	13	E. Allen Emerson , Aloysius K. Mok , A. Prasad Sistla , Jai Srinivasan, Quantitative Temporal Reasoning, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.136-145, June 18-21, 1990
	14	H. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.
	15	E. Hard, O. Lichtenstein, and A. Pnueli. Explicitclock temporal logic. In Proc. 5th 1EEE LICS, 1990.
	16	T. Henzinger. The Temporal Specification and Veri- Univ., 1991.
	17	T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model-checking for real-time systems, in Proc. 7th 1EEE LICS, 1992.
	18	J. Hooman, Specification and Compositional Verification of Real-Time Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1991
	19	Oscar H. Ibarra , Tao Jiang , Nicholas Q. Trân , Hui Wang, New Decidability Results Concerning Two-way Counter Machines and Applications, Proceedings of the 20th International Colloquium on Automata, Languages and Programming, p.313-324, July 05-09, 1993
	20	F. Jahanian. Verifying properties of systems with variable timing constraints. In Proc. l Oth IEEE RTSS, 1989.
	21	Ron Koymans, Specifying real-time properties with metric temporal logic, Real-Time Systems, v.2 n.4, p.255-299, Nov. 1990 [doi>10.1007/BF01995674]
	22	R. P. Kurshan, Analysis of discrete event coordination, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.414-453, May 1990, Mook, The Netherlands
	23	Leslie Lamport, A fast mutual exclusion algorithm, ACM Transactions on Computer Systems (TOCS), v.5 n.1, p.1-11, Feb. 1987 [doi>10.1145/7351.7352]
	24	N. Leveson and J. Stolzy. Analyzing safety and fault tolerance using timed Petri nets. In Proc. Int. Conf. Theory and Practice ol Software Development, LNCS 186. Springer, 1985.
	25	H. Lewis. A logic of concrete time intervals, in Proc. 5th IEEE LICS, 1990.
	26	L. Lipshitz. The diophantine problem for addition and divisibility. Trans. AMS, 235:271-283, 1978.
	27	Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
	28	Jonathan S. Ostroff, Temporal logic for real time systems, John Wiley & Sons, Inc., New York, NY, 1989
	29	Fred B. Schneider , Bard Bloom , Keith Marzullo, Putting Time into Proof Outlines, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.618-639, June 03-07, 1991
	30	R. Strong, D. Dolev, and F. Cristian. New latency bounds for atomic broadcast. In Proc. 11th IEEE RTSS, 1990.
	31	M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. 1st 1EEE LICS, 1986.
	32	F. Wang, A. Mok, and E. Emerson. Real-time distributed system specification and verification in APTL. In Proc. 12th lnt. Conf. Software Engineering, 1992.
	33	Henri B. Weinberg , Lenore D. Zuck, Timed Ethernet: Real-Time Formal Specification of Ethernet, Proceedings of the Third International Conference on Concurrency Theory, p.370-385, August 24-27, 1992

CITED BY 22

	Rajeev Alur , Thomas A. Henzinger, Finitary fairness, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.6, p.1171-1194, Nov. 1998
	Rajeev Alur , Kousha Etessami , Salvatore La Torre , Doron Peled, Parametric temporal logic for “model measuring”, ACM Transactions on Computational Logic (TOCL), v.2 n.3, p.388-407, July 2001
	Thomas A. Henzinger , Peter W. Kopke , Anuj Puri , Pravin Varaiya, What's decidable about hybrid automata?, Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, p.373-382, May 29-June 01, 1995, Las Vegas, Nevada, United States
	Farn Wang, Parametric Analysis of Computer Systems, Formal Methods in System Design, v.17 n.1, p.39-60, Aug. 2000
	Béatrice Bérard , Laurent Fribourg , Francis Klay , Jean-François Monin, A Compared Study of Two Correctness Proofs for the Standardized Algorithm of ABR Conformance, Formal Methods in System Design, v.22 n.1, p.59-86, January 2003
	Zhe Dang , Oscar H. Ibarra , Richard A. Kemmerer, Generalized discrete timed automata: decidable approximations for safety verification, Theoretical Computer Science, v.296 n.1, p.59-74, 4 March 2003
	Rajeev Alur , Thomas A. Henzinger , Pei-Hsin Ho, Automatic Symbolic Verification of Embedded Systems, IEEE Transactions on Software Engineering, v.22 n.3, p.181-201, March 1996
	Patricia Bouyer , Catherine Dufourd , Emmanuel Fleury , Antoine Petit, Updatable timed automata, Theoretical Computer Science, v.321 n.2-3, p.291-345, 16 August 2004
	Farn Wang, Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures, IEEE Transactions on Software Engineering, v.31 n.1, p.38-51, January 2005
	Farn Wang , Hsu-Chun Yen, Reachability solution characterization of parametric real-time systems, Theoretical Computer Science, v.328 n.1-2, p.187-201, 29 November 2004
	Tobias Amnell , Gerd Behrmann , Johan Bengtsson , Pedro R. D'Argenio , Alexandre David , Ansgar Fehnker , Thomas Hune , Bertrand Jeannet , Kim G. Larsen , M. Oliver Möller , Paul Pettersson , Carsten Weise , Wang Yi, UPPAAL: now, next, and future, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Holger Giese , Stefan Henkler , Martin Hirsch , Florian Klein, Nobody's perfect: interactive synthesis from parametrized real-time scenarios, Proceedings of the 2006 international workshop on Scenarios and state machines: models, algorithms, and tools, May 27-27, 2006, Shanghai, China
	Laurent Doyen, Robust parametric reachability for timed automata, Information Processing Letters, v.102 n.5, p.208-213, May, 2007
	Véronique Bruyère , Emmanuel Dall'olio , Jean-François Raskin, Durations and parametric model-checking in timed automata, ACM Transactions on Computational Logic (TOCL), v.9 n.2, p.1-23, March 2008
	Kathi Fisler, Timing Diagrams: Formalization and Algorithmic Verification, Journal of Logic, Language and Information, v.8 n.3, p.323-361, July 1999
	Anuj Puri, An Undecidable Problem for Timed Automata, Discrete Event Dynamic Systems, v.9 n.2, p.135-146, May 1999
	Slawomir Lasota , Igor Walukiewicz, Alternating timed automata, ACM Transactions on Computational Logic (TOCL), v.9 n.2, p.1-27, March 2008
	Robert Clarisó , Jordi Cortadella, Verification of Concurrent Systems with Parametric Delays Using Octahedra, Fundamenta Informaticae, v.78 n.1, p.1-33, January 2007
	Shinya Umeno, Event order abstraction for parametric real-time system verification, Proceedings of the 7th ACM international conference on Embedded software, October 19-24, 2008, Atlanta, GA, USA
	Étienne André , Thomas Chatain , Laurent Fribourg , Emmanuelle Encrenaz, An Inverse Method for Parametric Timed Automata, Electronic Notes in Theoretical Computer Science (ENTCS), 223, p.29-46, December, 2008
	Hsu-Chun Yen , Chien-Liang Chen, On minimal elements of upward-closed sets, Theoretical Computer Science, v.410 n.24-25, p.2442-2452, May, 2009
	Libor Waszniowski , Zdenĕk Hanzálek, Formal verification of multitasking applications based on timed automata model, Real-Time Systems, v.38 n.1, p.39-65, January 2008