Abstract
I develop a compositional theory of refinement for the branching time framework based on stuttering simulation and prove that if one system refines another, then a refinement map always exists. The existence of refinement maps in the linear time framework was studied in an influential paper by Abadi and Lamport. My interest in proving analogous results for the branching time framework arises from the observation that in the context of mechanical verification, branching time has some important advantages. By setting up the refinement problem in a way that differs from the Abadi and Lamport approach, I obtain a proof of the existence of refinement maps (in the branching time framework) that does not depend on any of the conditions found in the work of Abadi and Lamport e.g., machine closure, finite invisible nondeterminism, internal continuity, the use of history and prophecy variables, etc. A direct consequence is that refinement maps always exist in the linear time framework, subject only to the use of prophecy-like variables.
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82(2), 253–284 (1991)
Attie, P.C.: Liveness-preserving simulation relations. In: ACM Symposium on the Principles of Distributed Computing (PODC), May 1999, pp. 63-72 (1999)
Hasten, T.: Branching bisimilarity is an equivalence indeed. Information Processing Letters 58(3), 141–147 (1996)
Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Engelhardt, K., de Roever, W.-P.: Generalizing Abadi & Lamport’s method to solve a problem posed by Pnueli, A. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670, pp. 294–313. Springer, Heidelberg (1993)
Glabbeek, R.J.v.: The linear time - branching time spectrum I; the semantics of concrete, sequential processes. In: Handbook of Process Algebra, ch. 1, pp. 3–99. Elsevier, Amsterdam (2001)
Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: IEEE Symposium on Foundations of Computer Science, pp. 453–462. IEEE Computer Society Press, Los Alamitos (1995)
Hesselink, W.: Eternity variables to simulate specifications. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 117–130. Springer, Heidelberg (2002)
Jonsson, B., Pnueli, A., Rump, C.: Proving refinement using transduction. Distributed Computing 12(2-3), 129–149 (1999)
Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Moore, J.S.: ACL2 homepage, See http://www.es.-utexas.edu/users/moore/acl2
Kunen, K.: Set Theory - An Introduction to Independence Proofs. Studies in Logic and the Foundations of Mathematics, vol. 102. North-Holland, Amsterdam (1980)
Lamport, L.: What good is temporal logic? Information Processing 83, 657–688 (1983)
Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations - part I: untimed systems. Information and Computation 121(2), 214–233 (1995)
Manolios, P.: Correctness of pipelined machines. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 161–178. Springer, Heidelberg (2000)
Manolios, P., Namjoshi, K., Sumners, R.: Linking theorem proving and model-checking with well-founded bisimulation. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 369–379. Springer, Heidelberg (1999)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1990)
Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol. 1346, pp. 284–296. Springer, Heidelberg (1997)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM Journal on Computing 16(6), 973–989 (1987)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, pp. 46–57. IEEE, Los Alamitos (1977)
Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 15–32. Springer, Heidelberg (1985)
Sawada, J.: Formal Verification of an Advanced Pipelined Machine. PhD thesis, University of Texas at Austin (December 1999)
Sawada, J.: Verification of a simple pipelined machine model. In: Kaufmann et al. [10], pp. 137–150
Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time. In: STOC: ACM Symposium on Theory of Computing (STOC), pp. 1-9 (1973)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manolios, P. (2003). A Compositional Theory of Refinement for Branching Time. In: Geist, D., Tronci, E. (eds) Correct Hardware Design and Verification Methods. CHARME 2003. Lecture Notes in Computer Science, vol 2860. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39724-3_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-39724-3_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20363-6
Online ISBN: 978-3-540-39724-3
eBook Packages: Springer Book Archive