Abstract
This paper presents a method for the decomposition of HML formulae. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulae, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is that an earlier decomposition method from Larsen [14] for the De Simone format is extended to the more general ntyft/ntyxt format without lookahead.
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.
Similar content being viewed by others
References
Andersen, H.R., Stirling, C., Winskel, G.: Compositional proof system for the modal μ-calculus. In: Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 144–153. IEEE Computer Society Press, Paris (1994)
Andersen, H.R., Winskel, G.: Compositional checking of satisfaction. Formal Methods in System Design 1(4), 323–354 (1992)
Barringer, H., Kuiper, R., Pnueli, A.: Now you may compose temporal logic specifications. In: ACM Symposium on Theory of Computing (STOC 1984), pp. 51–63. ACM Press, Baltimore (1984)
Bloom, B., Fokkink, W.J., van Glabbeek, R.J.:: Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic (2003) (to appear)
Bol, R., Groote, J.F.: The meaning of negative premises in transition system specifications. Journal of the ACM 43(5), 863–914 (1996)
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31(3), 560–599 (1984)
van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 502–513. Springer, Heidelberg (1996)
van Glabbeek, R.J.: The linear time – branching time spectrum I: The semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 1, pp. 3–99. Elsevier, Amsterdam (2001)
Groote, J.F.: Transition system specifications with negative premises. Theoretical Computer Science 118(2), 263–299 (1993)
Harel, D., Kozen, D., Parikh, R.: Process logic: Expressiveness, decidability, completeness. Journal of Computer and System Sciences 25(2), 144–170 (1982)
Hennessy, M.C.B., Milner, R.: Algebraic laws for non-determinism and concurrency. Journal of the ACM 32(1), 137–161 (1985)
Hennessy, M.C.B., Stirling, C.: The power of the future perfect in program logics. Information and Control 67(1-3), 23–52 (1985)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27(3), 333–354 (1983)
Larsen, K.G.: Context-Dependent Bisimulation between Processes. PhD thesis, University of Edinburgh, Edinburgh (1986)
Larsen, K.G., Xinxin, L.: Compositionality through an operational semantics of contexts. Journal of Logic and Computation 1(6), 761–795 (1991)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Milner, R.: A modal characterization of observable machine-behaviour. In: Astesiano, E., Böhm, C. (eds.) CAAP 1981. LNCS, vol. 112, pp. 25–34. Springer, Heidelberg (1981)
Milner, R.: Calculi for synchrony and asynchrony. Theoretical Computer Science 25(3), 267–310 (1983)
Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark (1981)
Pnueli, A.: The temporal logic of concurrent programs. Theoretical Computer Science 13, 45–60 (1981)
De Simone, R.: Higher-level synchronising devices in Meije–SCCS. Theoretical Computer Science 37(3), 245–267 (1985)
Stirling, C.: A proof-theoretic characterization of observational equivalence. Theoretical Computer Science 39(1), 27–45 (1985)
Stirling, C.: A complete compositional modal proof system for a subset of CCS. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 475–486. Springer, Heidelberg (1985)
Stirling, C.: A complete modal proof system for a subset of SCCS. In: Nivat, M., Floyd, C., Thatcher, J., Ehrig, H. (eds.) CAAP 1985 and TAPSOFT 1985. LNCS, vol. 185, pp. 253–266. Springer, Heidelberg (1985)
Stirling, C.: Modal logics for communicating systems. Theoretical Computer Science 49(2-3), 311–347 (1987)
Winskel, G.: A complete proof system for SCCS with modal assertions. Fundamenta Informaticae IX, 401–420 (1986)
Winskel, G.: On the compositional checking of validity (extended abstract). In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 481–501. Springer, Heidelberg (1990)
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
Fokkink, W., van Glabbeek, R., de Wind, P. (2003). Compositionality of Hennessy-Milner Logic through Structural Operational Semantics. In: Lingas, A., Nilsson, B.J. (eds) Fundamentals of Computation Theory. FCT 2003. Lecture Notes in Computer Science, vol 2751. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45077-1_38
Download citation
DOI: https://doi.org/10.1007/978-3-540-45077-1_38
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40543-6
Online ISBN: 978-3-540-45077-1
eBook Packages: Springer Book Archive