×

zbMATH — the first resource for mathematics

The cones and foci proof technique for timed transition systems. (English) Zbl 1003.68092
Summary: We propose an extension of the cones and foci proof technique that can be used to prove timed branching bisimilarity of states in timed transition systems. We prove the correctness of this technique and we give an example verification.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baeten, J.C.M.; Bergstra, J.A., Real time process algebra, Formal aspects comput., 3, 2, 142-188, (1991) · Zbl 0719.68020
[2] Baeten, J.C.M.; Bergstra, J.A., Discrete time process algebra, Formal aspects comput., 8, 2, 188-208, (1996) · Zbl 0849.68033
[3] Baeten, J.C.M.; Bergstra, J.A.; Reniers, M.A., Discrete time process algebra with silent step, (), 535-569, Chapter 18
[4] Bergstra, J.A.; Klop, J.W., Process algebra for synchronous communication, Inform. and control, 60, 1-3, 109-137, (1984) · Zbl 0597.68027
[5] Fokkink, W., Introduction to process algebra, Texts in theoretical computer science, (2000), Springer Berlin
[6] Fokkink, W.J., An axiomatization for regular processes in timed branching bisimulation, Fund. inform., 32, 329-340, (1997) · Zbl 0926.68054
[7] Fredlund, L.-Å.; Groote, J.F.; Korver, H.P., Formal verification of a leader election protocol in process algebra, Theoret. comput. sci., 177, 459-486, (1997) · Zbl 0911.68057
[8] van Glabbeek, R.J.; Weijland, W.P., Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600, (1996) · Zbl 0882.68085
[9] Groote, J.F., The syntax and semantics of timed \(μ\)CRL, technical report SEN-R9709, (1997), CWI Amsterdam
[10] Groote, J.F.; Monin, F.; van de Pol, J.C., Checking verifications of protocols and distributed systems by computer, (), 629-655
[11] Groote, J.F.; Ponse, A., The syntax and semantics of \(μ\)CRL, (), 26-62
[12] Groote, J.F.; Reniers, M.A.; van Wamel, J.; van der Zwaag, M.B., Completeness of timed \(μ\)CRL, technical report SEN-R0034, (2000), CWI Amsterdam · Zbl 1011.68063
[13] Groote, J.F.; Springintveld, J., Focus points and convergent process operators. A proof strategy for protocol verification, Logic group preprint series 142, (1995), Department of Philosophy, Utrecht University
[14] Groote, J.F.; Springintveld, J., Algebraic verification of a distributed summation algorithm, technical report CS-R9640, (1996), CWI Amsterdam
[15] Hoare, C.A.R., Communicating sequential processes, (1985), Prentice-Hall Englewood Cliffs, NJ · Zbl 0637.68007
[16] Klusener, A.S., The silent step in time, (), 421-435
[17] Klusener, A.S., Models and axioms for a fragment of real time process algebra, phd thesis, (1993), Eindhoven University of Technology
[18] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood Cliffs, NJ · Zbl 0683.68008
[19] Moller, F.; Tofts, C., A temporal calculus of communicating systems, (), 401-415
[20] Reed, G.M.; Roscoe, A.W., A timed model for communicating sequential processes, Theoret. comput. sci., 58, 1-3, 249-261, (1998) · Zbl 0655.68031
[21] Shankland, C.; van der Zwaag, M.B., The tree identify protocol of IEEE 1394 in \(μ\)CRL, Formal aspects comput., 10, 509-531, (1998) · Zbl 0951.68532
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.