Abstract
To develop efficient algorithms for the reachability analysis of timed automata, a promising approach is to use binary decision diagrams (BDDs) as data structure for the representation of the explored state space. The size of a BDD is very sensitive to the ordering of the variables. We use the communication structure to deduce an estimation for the BDD size. In our experiments, this guides the choice of good variable orderings, which leads to an efficient reachability analysis. We develop a discrete semantics for closed timed automata to get a finite state space required by the BDD-based representation and we prove the equivalence to the continuous semantics regarding the set of reachable locations. An upper bound for the size of the BDD representing the transition relation and an estimation for the set of reachable configurations based on the communication structure is given. We implemented these concepts in the verification tool Rabbit [BR00]. Different case studies justify our conjecture: Polynomial reachability analysis seems to be possible for some classes of real-time models, which have a good-natured communication structure.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
[ABK+97]_Eugene Asarin, Marius Bozga, Alain Kerbat, Oded Maler, Amir Pnueli, and Anne Rasse. Data-structures for the verification of timed automata. In O. Maler, editor, Proceedings of the 1st International Workshop on Hybrid and Real-Time Systems (HART’97), LNCS 1201, pages 346–360. Springer-Verlag, 1997.
Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
Eugene Asarin, Oded Maler, and Amir Pnueli. On discretization of delays in timed automata and digital circuits. In R. de Simone and D. Sangiorgi, editors, Proceedings of the 9th International Conference on Concurrency Theory (CONCUR’98), LNCS 1466, pages 470–484. Springer-Verlag, 1998.
Adnan Aziz, Serdar Tasiran, and Robert K. Brayton. BDD variable ordering for interacting finite state machines. In Proceedings of the 31st ACM/IEEE Design Automation Conference (DAC’94), pages 283–288, 1994.
Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. Kronos: a model-checking tool for real-time systems. In A.J. Hu and M.Y. Vardi, editors, Proceedings of the 10th International Conference on Computer-Aided Veri_cation (CAV’98), LNCS 1427, pages 546–550. Springer-Verlag, 1998.
Marius Bozga, Oded Maler, Amir Pnueli, and Sergio Yovine. Some progress on the symbolic verification of timed automata. In O. Grumberg, editor, Proceedings of the 9th International Conference on Computer Aided Verification (CAV’97), LNCS 1254, pages 179–190. Springer-Verlag, 1997.
Dirk Beyer and Heinrich Rust. Modeling a production cell as a distributed real-time system with cottbus timed automata. In Hartmut König and Peter Langendörfer, editors, Tagungsband Formale Beschreibungstechniken für verteilte Systeme (FBT’98), pages 148–159. Shaker Verlag, Aachen, June 1998.
Dirk Beyer and Heinrich Rust. A formalism for modular modelling of hybrid systems. Technical Report 10/1999, BTU Cottbus, 1999.
Dirk Beyer and Heinrich Rust. A tool for modular modelling and verification of hybrid systems. In Alfons Crespo and Joan Vila, editors, Proceedings of the 25th IFAC/IFIP Workshop on Real-Time Programming 2000 (WRTP 2000). Elsevier Science, Oxford, 2000.
Karl S. Brace, Richard L. Rudell, and Randal E. Bryant. Efficient implementation of a BDD package. In Proceedings of the 27th ACM/IEEE Design Automation Conference (DAC’90), pages 40–45, 1990.
Aleks Göllü, Anuj Puri, and Pravin Varaiya. Discretization of timed automata. In Proceedings of the 33rd IEEE Conference on Decision and Control, pages 957–958, 1994.
Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. What good are digital clocks? In Proceedings of the 19th International Colloquium on Automata, Languages, and Programming (ICALP’92), LNCS 623, pages 545–558. Springer-Verlag, 1992.
Leslie Lamport. A fast mutual exclusion algorithm. ACM Transactions on Computer Systems, 5(1):1–11, 1987.
E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, and D. B. Shmoys, editors. The Traveling Salesman Problem. John Wiley & Sons, 1985.
Kim G. Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a Nut-shell. International Journal on Software Tools for Technology Transfer, 1(1-2):134–152, October 1997.
Kenneth L. McMillan. Symbolic Model Checking: an approach to the state explosion problem. PhD thesis, School of Computer Science, Carnegie Mellon University, 1992. Technical report CMU-CS-92-131.
Rajeev K. Ranjan, Adnan Aziz, Robert K. Brayton, Carl Pixley, and Bernhard Plessier.Efficient BDD algorithms for synthesizing and verifying finite state machines. In Workshop Notes of the IEEE/ACM International Workshop on Logic Synthesis (IWLS’95), 1995.
Bwolen Yang, Randal E. Bryant, David R. O’Hallaron, Armin Biere, Olivier Coudert, Geert Janssen, Rajeev K. Ranjan, and Fabio Somenzi. A performance study of BDD-based model checking. In Ganesh Gopalakrishnan and Phillip J. Windley, editors, Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design (FMCAD’98), LNCS 1522, pages 255289. Springer-Verlag, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beyer, D. (2001). Improvements in BDD-Based Reachability Analysis of Timed Automata. In: Oliveira, J.N., Zave, P. (eds) FME 2001: Formal Methods for Increasing Software Productivity. FME 2001. Lecture Notes in Computer Science, vol 2021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45251-6_18
Download citation
DOI: https://doi.org/10.1007/3-540-45251-6_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41791-0
Online ISBN: 978-3-540-45251-5
eBook Packages: Springer Book Archive