Abstract
We describe the design of abstraction methods based on symbolic techniques: classical abstraction by state fusion has been considered. We present a general method to abstract automata on the basis of a state fusion criterion, derived from e.g. equivalence relations (such as bisimulation), partitions, … We also introduce other kinds of abstraction, falling into the category of abstraction by restriction: in particular, we study the use of the controller synthesis methodology to achieve the restriction synthesis.
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.
References
Alur, R., Henzinger, T. A., and Kupferman, O. (1998). Alternating-time temporal logic. Lecture Notes in Computer Science, 1536:23–60.
Bensalem, S., Lakhnech, Y., and Owre, S. (1998). Computing abstractions of infinite state systems compositionally and automatically. In Conference on Computer Aided Verification CAV’98, LNCS 1427, pages 319–331.
Bryant, R. (1986). Graph-based algorithms for boolean function manipulations. IEEE Transaction on Computers, C-45(8):677–691.
Burch, J., Clarke, E., McMillan, K., Dill, D., and Hwang, L. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170.
Clarke, E., Grumberg, O., and Long, D. (1994). Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542.
Clarke, E. and Kurshan, R., editors (1990). Proc. of the 2nd Work. on Computer-Aided Verification, LNCS 531. Springer-Verlag.
Clarke, E., Long, D., and Mc Millan, K. (1989). A language for compositional specification and verification of finite state hardware controllers. In Proc. of the 9th Int. Symp. on Computer Hardware Description Languages and Their Applications, pages 281–295.
Cousot, P. and Cousot, R. (2000). Temporal abstract interpretation. In Conference Record of the 27th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, pages 12–25, New York, U.S.A. ACM Press.
Godefroid, P. (1990). Using partial orders to improve automatic verification methods. In Proc. of the 2nd Work, on Computer-Aided Verification, LNCS 531, pages 176–185. Springer-Verlag.
Kouchnarenko, O. and Pinchinat, S. (1998). Intensional approachs for symbolic methods. Electronic Notes in TCS, 18. http://www.elsevier.nl/locate/entcs/volumel8.html.
Kozen, D. (1983). Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333–354.
Larsen, K. G. (1989). Modal specifications. In Proc. Workshop Automatic Verification Methods for Finite State Systems, Grenoble, LNCS 407, pages 232–246. Springer-Verlag.
Manna, Z. and Pnueli, A. (1992). The Temporal Logic of Reactive and Concurrent Systems, volume I: Specification. Springer-Verlag.
Marchand, H. and Le Borgne, M. (1999). The supervisory control problem of discrete event systems using polynomial methods. Research Report 1271, Irisa.
McMillan, K. (1993). Symbolic Model Checking: An Approach to the state explosion problem. Kluwer Academic.
Milner, R. (1989). A complete axiomatisation for observational congruence of finite-state behaviours. SIAM J. Comput., 81(2):227–247.
Park, D. (1981). Concurrency and automata on infinite sequences. In Proc. 5th GI Conf. on Th. Comp. Set., LNCS 104, pages 167–183. Springer-Verlag.
Peled, D. (1994). Combining partial order reductions with on-the-fly model-checking. In Proc. of Worshop on Computer Aided Verification CAV’94, LNCS 818, pages 377–390.
Pinchinat, S., Marchand, H., and Le Borgne, M. (1999). Symbolic abstractions of automata and their application to the supervisory control problem. Research Report 1279, IRISA.
Ramadge, P. J. and Wonham, W. M. (1989). The control of discrete event systems. Proceedings of the IEEE; Special issue on Dynamics of Discrete Event Systems, 77(1):81–98.
Van Glabbeek, R. J. (1993). The linear time-branching time spectrum II: The semantics of sequential systems with silent moves (extended abstract). In CONCUR’ 93, volume 715 of LNCS, pages 66–81, Hildesheim, Germany. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
Pinchinat, S., Marchand, H. (2000). Symbolic Abstractions of Automata. In: Boel, R., Stremersch, G. (eds) Discrete Event Systems. The Springer International Series in Engineering and Computer Science, vol 569. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-4493-7_3
Download citation
DOI: https://doi.org/10.1007/978-1-4615-4493-7_3
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-7025-3
Online ISBN: 978-1-4615-4493-7
eBook Packages: Springer Book Archive