Abstract
In this paper we show how to use McMillan’s complete finite prefix approach for process algebra. We present the model of component event structures as a semantics for process algebra, and show how to construct a complete finite prefix for this model. We present a simple adequate order (using an order on process algebra expressions) as an optimization to McMillan’s original algorithm
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
T. Bolognesi and E. Brinksma. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 14:25–59, 1987.
G. Boudol and I. Castellani. Flow models of distributed computations: three equivalent semantics for CCS. Information and Computation, 114:247–314, 1994.
E. Brinksma, J.-P. Katoen, D. Latella, and R. Langerak. Partial-order models for quantitative extensions of LOTOS. Computer Networks and ISDN Systems, 30(9/10):925–950, 1998.
J.C.M. Baeten and W.P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.
J. Engelfriet. Branching processes of Petri nets. Acta Informatica, 28:575–591, 1991.
J. Esparza, S. Römer, and W. Vogler. An improvement of McMillan’s unfolding algorithm. In Proc. TACAS’ 96, volume 1055 of Lecture Notes in Computer Science, pages 87–106. Springer-Verlag, 1997.
J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23(2):151–195, 1994. Also appeared in Proc. TAPSOFT’ 93, volume 668 of Lecture Notes in Computer Science, pages 613-628. Springer-Verlag, 1993.
A. Fantechi, S. Gnesi, and G. Mazzarini. The expressive power of LOTOS behaviour expressions. Nota Interna I.E.I. B4-43, I.E.I (Pisa), October 1992.
B. Graves. Computing reachability properties hidden in finite net unfoldings. Lecture Notes in Computer Science, 1055:327–342, 1997.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
[KLL+98]_ J.-P. Katoen, D. Latella, R. Langerak, E. Brinksma, and T. Bolognesi. A consistent causality-based view on a timed process algebra including urgent interactions. Journal on Formal Methods for System Design, 12(2):189–216, 1998.
R. Langerak. Transformations and Semantics for LOTOS. PhD thesis, University of Twente, 1992.
R. Langerak and E. Brinksma. A complete finite prefix for process algebra. Technical report, University of Twente, January 1999.
K. McMillan. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. CAV’ 92, Fourth Workshop on Computer-Aided Verification, volume 663 of Lecture Notes in Computer Science, pages 164–174, 1992.
K. McMillan. Trace theoretic verification of asynchronous circuits using unfoldings. In Proc. CAV’ 95, 7th International Conference on Computer-Aided Verification, volume 939 of Lecture Notes in Computer Science, pages 180–195. Springer-Verlag, 1995.
K.L. McMillan. A technique of state space search based on unfolding. Formal Methods in System Design, 6:45–65, 1995.
M. Nielsen, G.D. Plotkin, and G. Winskel. Petri nets, event structures and domains, part 1. Theoretical Computer Science, 13(1):85–108, 1981.
E.-R. Olderog. Nets, terms and formulas. Cambridge University Press, 1991.
F. Wallner. Model-checking LTL using net unfoldings. In Proc. CAV’ 98, 10th International Conference on Computer-Aided Verification, volume 1427 of Lecture Notes in Computer Science, pages 207–218, Vancouver, Canada, 1998.
G. Winskel. An introduction to event structures. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Lecture Notes in Computer Science, pages 364–397. Springer-Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Langerak, R., Brinksma, E. (1999). A Complete Finite Prefix for Process Algebra. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_18
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive