Document Zbl 1277.68182

Fokkink, Wan; van Glabbeek, Rob; de Wind, Paulien

Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity. (English) Zbl 1277.68182

Inf. Comput. 214, 59-85 (2012).

Summary: We present a method for decomposing modal formulas for processes with the internal action \(\tau \). To decide whether a process algebra term satisfies a modal formula, one can check whether its subterms satisfy formulas that are obtained by decomposing the original formula. The decomposition uses the structural operational semantics that underlies the process algebra. We use this decomposition method to derive congruence formats for two weak and rooted weak semantics: branching and \(\eta \)-bisimilarity.

Cited in 4 Reviews

Cited in 13 Documents

MSC:

68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B45	Modal logic (including the logic of norms)
68Q55	Semantics in the theory of computing

Keywords:

structural operational semantics; modal logic; process algebra; process semantics; congruence

Cite Review PDF

Full Text: DOI

References:

[1]	Baeten, J. C.M.; Bergstra, J. A.; Klop, J. W., Syntax and defining equations for an interrupt mechanism in process algebra, Fund. Inform., 9, 2, 127-167 (1986) · Zbl 0617.68027
[2]	Baeten, J. C.M.; van Glabbeek, R. J., Another look at abstraction in process algebra, (Proc. ICALPʼ87. Proc. ICALPʼ87, Lecture Notes in Comput. Sci., vol. 267 (1987), Springer), 84-94 · Zbl 0623.68023
[3]	Basten, T., Branching bisimulation is an equivalence indeed!, Inform. Process. Lett., 58, 3, 141-147 (1996) · Zbl 0875.68624
[4]	Bergstra, J. A.; Klop, J. W., Process algebra for synchronous communication, Inf. Control, 60, 1-3, 109-137 (1984) · Zbl 0597.68027
[5]	Bloom, B., Structural operational semantics for weak bisimulations, Theoret. Comput. Sci., 146, 1-2, 25-68 (1995) · Zbl 0873.68130
[6]	Bloom, B.; Fokkink, W. J.; van Glabbeek, R. J., Precongruence formats for decorated trace semantics, ACM Trans. Comput. Log., 5, 1, 26-78 (2004) · Zbl 1367.68209
[7]	Bloom, B.; Istrail, S.; Meyer, A. R., Bisimulation canʼt be traced, J. ACM, 42, 1, 232-268 (1995) · Zbl 0886.68027
[8]	Bol, R. N.; Groote, J. F., The meaning of negative premises in transition system specifications, J. ACM, 43, 5, 863-914 (1996) · Zbl 0889.68113
[9]	De Nicola, R.; Vaandrager, F. W., Three logics for branching bisimulation, J. ACM, 42, 2, 458-487 (1995) · Zbl 0886.68064
[10]	Fokkink, W. J., Rooted branching bisimulation as a congruence, J. Comput. System Sci., 60, 1, 13-37 (2000) · Zbl 0955.68074
[11]	Fokkink, W. J.; van Glabbeek, R. J., Ntyft/ntyxt rules reduce to ntree rules, Inform. and Comput., 126, 1, 1-10 (1996) · Zbl 0853.68124
[12]	Fokkink, W. J.; van Glabbeek, R. J.; de Wind, P., Compositionality of Hennessy-Milner logic by structural operational semantics, Theoret. Comput. Sci., 354, 3, 421-440 (2006) · Zbl 1088.68094
[13]	Fokkink, W. J.; van Glabbeek, R. J.; de Wind, P., Divide and congruence: From decomposition of modalities to preservation of branching bisimulation, (Proc. FMCOʼ05. Proc. FMCOʼ05, Lecture Notes in Comput. Sci., vol. 4111 (2006), Springer), 195-218 · Zbl 1196.68156
[14]	Fokkink, W. J.; van Glabbeek, R. J.; de Wind, P., Divide and congruence applied to \(η\)-bisimulation, (Proc. SOSʼ05. Proc. SOSʼ05, Electron. Notes Theor. Comput. Sci., vol. 156 (1) (2006), Elsevier), 97-113 · Zbl 1273.68257
[15]	van Gelder, A.; Ross, K.; Schlipf, J. S., The well-founded semantics for general logic programs, J. ACM, 38, 3, 620-650 (1991) · Zbl 0799.68045
[16]	van Glabbeek, R. J., Bounded nondeterminism and the approximation induction principle in process algebra, (Proc. STACSʼ87. Proc. STACSʼ87, Lecture Notes in Comput. Sci., vol. 247 (1987), Springer), 336-347 · Zbl 0612.68025
[17]	van Glabbeek, R. J., The linear time-branching time spectrum II: The semantics of sequential systems with silent moves, (Proc. CONCURʼ93. Proc. CONCURʼ93, Lecture Notes in Comput. Sci., vol. 715 (1993), Springer), 66-81
[18]	van Glabbeek, R. J., The meaning of negative premises in transition system specifications II, J. Log. Algebr. Program., 60-61, 229-258 (2004) · Zbl 1072.68075
[19]	van Glabbeek, R. J., On cool congruence formats for weak bisimulations, Theoret. Comput. Sci., 412, 28, 3283-3302 (2011) · Zbl 1216.68199
[20]	van Glabbeek, R. J.; Weijland, W. P., Branching time and abstraction in bisimulation semantics, J. ACM, 43, 3, 555-600 (1996) · Zbl 0882.68085
[21]	Groote, J. F., Transition system specifications with negative premises, Theoret. Comput. Sci., 118, 2, 263-299 (1993) · Zbl 0778.68057
[22]	Groote, J. F.; Vaandrager, F. W., Structured operational semantics and bisimulation as a congruence, Inform. and Comput., 100, 2, 202-260 (1992) · Zbl 0752.68053
[23]	Hennessy, M.; Milner, R., Algebraic laws for non-determinism and concurrency, J. ACM, 32, 1, 137-161 (1985) · Zbl 0629.68021
[24]	Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice Hall · Zbl 0637.68007
[25]	Kleene, S. C., Representation of events in nerve nets and finite automata, (Shannon, C.; McCarthy, J., Automata Studies (1956), Princeton University Press), 3-41 · Zbl 0061.01003
[26]	Larsen, K. G.; Liu, X., Compositionality through an operational semantics of contexts, J. Logic Comput., 1, 6, 761-795 (1991) · Zbl 0738.68056
[27]	Milner, R., A modal characterisation of observable machine-behaviour, (Proc. CAAPʼ81. Proc. CAAPʼ81, Lecture Notes in Comput. Sci., vol. 112 (1981), Springer), 25-34 · Zbl 0474.68074
[28]	Milner, R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008
[29]	Milner, R., Communicating and Mobile Systems: The \(π\)-Calculus (1999), Cambridge University Press · Zbl 0942.68002
[30]	Plotkin, G. D., A structural approach to operational semantics, J. Log. Algebr. Program., 60-61, 17-139 (2004), originally appeared in 1981 · Zbl 1082.68062
[31]	de Simone, R., Higher-level synchronising devices in Meije-SCCS, Theoret. Comput. Sci., 37, 3, 245-267 (1985) · Zbl 0598.68027
[32]	F.W. Vaandrager, Algebraic techniques for concurrency and their application, PhD thesis, University of Amsterdam, 1990.; F.W. Vaandrager, Algebraic techniques for concurrency and their application, PhD thesis, University of Amsterdam, 1990.

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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.