×

zbMATH — the first resource for mathematics

A modal logic for message passing processes. (English) Zbl 0827.68102
Summary: A first-order modal logic is given for describing properties of processes which may send and receive values or messages along communication ports. We give two methods for proving that a process enjoys such a property. The first is the construction, for each process \(P\) and formula \(F\), of a characteristic formula \(P \text{ sat } F\) such that \(P\) enjoys the property \(F\) if and only if the formula \(P \text{ sat }F\) is logically equivalent to \(\mathbf t\mathbf t\). The second is a sound and complete proof system whose judgements take the form \(B \vdash P : F\), meaning: under the assumption \(B\) the process \(P\) enjoys the property \(F\). The notion of symbolic operational semantics plays a crucial role in the design of both the characteristic formulae and the proof system.

MSC:
68T27 Logic in artificial intelligence
03B45 Modal logic (including the logic of norms)
Software:
LOTOS
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] R. Cleaveland, J. Parrow, B. Steffen: The concurrency workbench. University of Edinburgh, Scotland, 1988
[2] J.C. Godskesen, K.G. Larsen, M. Zeeberg: Tav – tools for automatic verification – users manual. Technical Report R 89-19, Department of Matheamtics and Computer Science, Aalborg University, 1989. Presented at workshop on Automatic Methods for Finite State, Systems, Grenoble, France, Juni 1989
[3] S. Graf, J. Sifakis: A logic for the description of non-deterministic programs and their properties. Information and Control, 68 (1–3), 1986
[4] M. Hennessy: A proof system for communicating processes with value-passing.Formal Aspects of Computer Science, 3:346–366, 1991 · Zbl 0736.68057 · doi:10.1007/BF01642508
[5] M. Hennessy, H. Lin: Symbolic bisimulation. Technical Report Technical Report 1/92, School of Congnitive and Computing Sciences, University of Sussex, 1992
[6] M. Hennessy, X. Liu: A modal logic for message passing processes. Technical Report Technical Report 3/93, School of Congnitive and Computing Sciences, University of Sussex 1993
[7] A. Ingolfsdottir, B. Thomsen: Semantic models for ccs with values. Technical Report 63, Programming Methodology Group, Chalmers University of Technology, 1992. In Proceedings of the Workshop on Concurrency
[8] K.G. Larsen: Proof systems for Hennessy-Milner logic with recursion.Lecture Notes In Computer Science, Springer Verlag, 299, 1988. in Proceedings of 13th Colloquium on Trees in Algebra and Programming 1988 · Zbl 0647.68012
[9] H. Lin: A verification tool for value-passing processes. Technical report, School of Congnitive and Computing Sciences, University of Sussex, 1993. To appear
[10] R. Milner:Communication and Concurrency. Prentice-Hall, 1989 · Zbl 0683.68008
[11] R. Milner, J. Parrow, D. Walker: Modal logics for mobile processes.Theoretical Computer Science, 1992. To appear · Zbl 0778.68033
[12] B. Steffen, A. Ingolfsdottir: Characteristic formulae for processes with divergence. Technical Report Technical Report 1/91, School of Congnitive and Computing Sciences, University of Sussex, 1991
[13] C. Stirling: Modal logics for communicating systems.Theoretical Computer Science, (311–347), 1987 · Zbl 0624.68019
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.