Cited By
View all- El-Qurna JYahyaoui HAlmulla M(2017)A new framework for the verification of service trust behaviorsKnowledge-Based Systems10.1016/j.knosys.2017.01.011121:C(7-22)Online publication date: 1-Apr-2017
Compositionality of fixpoint logic with chop
Authors: 
Naijun Zhan, Jinzhao WuAuthors Info & Claims
Pages 136 - 150
Abstract
Compositionality plays an important role in designing reactive systems as it allows one to compose/decompose a complex system from/to several simpler components. Generally speaking, it is hard to design a complex system in a logical frame in a compositional way because it is difficult to find a connection between the structure of a system to be developed and that of its specification given by the logic. In this paper, we investigate the compositionality of the Fixpoint Logic with Chop (FLC for short). To this end, we extend FLC with the nondeterministic choice “+” (FLC+ for the extension) and then establish a correspondence between the logic and the basic process algebra with deadlock and termination (abbreviated BPA$^{\epsilon}_{\delta}$). Subsequently, we show that the choice “+” is definable in FLC.
As an application of the compositionality of FLC, an algorithm is given to construct characteristic formulae of BPA$^{\epsilon}_{\delta}$ up to strong bisimulation directly from the syntax of processes in a compositional manner.
References
[1]
L. Aceto and M. Hennessy. Termination, deadlock, and divergence. Journal of ACM, Vol. 39, No.1: 147-187. January, 1992.
[2]
H.R. Andersen, C. Stirling, G. Winskel. A compositional proof system for the modal mu-Calculus. LICS'94, pp.144-153.
[3]
H. Barringer, R. Kuiper, A. Pnueli. Now you may compose temporal logic specifications. In Proc. 16th STOC, pp. 51-63. 1984.
[4]
H. Barringer, R. Kuiper, A. Pnueli. A compositional temporal approach to a CSP-like language. In Proc. IFIP conference, The Role of Abstract Models in Information Processing, pp. 207-227. 1985.
[5]
J.A. Bergstra and J.W. Klop. Algebra of communication processes with abstraction. Theoretical Computer Science, 37:77-121. 1985.
[6]
A. Chandra, J. Halpern, A. Meyer and R. Parikh. Equations between regular terms and an application to process logic. In Proc. 13th STOC, pp.384-390. 1981.
[7]
B. Dutertre. On first order interval logic. LICS'95, pp. 36-43, 1995.
[8]
E.A. Emerson and C.S. Jutla. Tree automata, µ-calculus, and determinacy. In Proc. 33rd FOCS, pp.368-377. 1991.
[9]
S. Graf and J. Sifakis. A modal characterization of observational congruence on finite terms of CCS. Information and Control, 68:125-145. 1986.
[10]
S. Graf and J. Sifakis. A logic for the description of non-deterministic programs and their properties. Information and Control, 68:254-270. 1986.
[11]
J. Halpern, B. Moskowski, and Z. Manna. A hardware semantics based on temporal intervals. ICALP'83, LNCS 154, pp. 278-291, 1983.
[12]
D. Harel, D. Kozen and R. Parikh. Process Logic: Expressiveness, decidability, completeness. In IEEE FOCS'80, pp. 129-142. 1980.
[13]
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
[14]
D. Janin and I. Walukiewicz. On the expressive completeness of the propositional µ-calculus with respect to monadic second order logic. CONCUR'96, LNCS 1119, pp.263-277. 1996.
[15]
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333-354. 1983.
[16]
M. Lange and C. Stirling. Model checking fixed point logic with chop. FOSSACS'02, LNCS 2303, pp. 250-263. 2002.
[17]
M. Lange. Local model checking games for fixed point logic with chop. CONCUR' 02, LNCS 2421, pp. 240-254. 2002.
[18]
K.G. Larsen and B. Thomsen. A modal process logic. In the proc. of LICS'88, pp.203-210. 1988.
[19]
K.G. Larsen and X.X. Liu. Compositionality through an operational semantics of contexts. ICALP'90, LNCS 443, pp.526-539. 1990.
[20]
K.G. Larsen and X.X. Liu. Equation solving using modal transition systems. LICS'90, pp. 108-107. 1990.
[21]
M. Müller-Olm. A modal fixpoint logic with chop. STACS'99, LNCS 1563, pp.510- 520. 1999.
[22]
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
[23]
A. Pnueli. The temporal logic of programs. In Proc. 18th STOC, pp.232-239. 1977.
[24]
R. Rosner and A. Pnueli. A choppy logic. In the proc. of LICS'86, pp.306-313. 1986.
[25]
B. Steffen, A. Ingólfsdóttir. Characteristic formulae for processes with divergence. Information and Computation, 110:149-163. 1994.
[26]
M. Viswanathan and R. Viswanathan. Foundations for circular compositional reasoning. ICALP'01, LNCS 2076, pp. 835-847, 2001.
[27]
Naijun Zhan. Compositional properties of sequential processes. In the proc. of SVV'03, ENTCS 118, pp.111-128. 2005.
[28]
C.C. Zhou, C.A.R. Hoare, and A. Ravn. A calculus of durations. Information Processing Letters, 40(5):269-276, 1991.
Index Terms
- Compositionality of fixpoint logic with chop
Index terms have been assigned to the content through auto-classification.
Recommendations
Compositional Properties of Sequential Processes
It is widely agreed that the modular method is one of the most effective methods to specify and verify complex systems in order to avoid combinatorial explosion. FLC ( Fixpoint Logic with Chop) is an important modal logic because of its expressivity and ...
A Characterisation Theorem for Two-Way Bisimulation-Invariant Monadic Least Fixpoint Logic Over Finite Structures
LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer ScienceA seminal theorem by van Benthem characterises the bisimulation-invariant fragment of First Order Logic (FOL) in terms of Modal Logic. Similarly, Janin and Walukiewicz have shown that the bisimulation-invariant fragment of Monadic Second Order Logic (MSO)...
Hybrid Logic Meets IF Modal Logic
The hybrid logic $${\mathcal{H}(@,\downarrow)}$$ and the independence friendly modal logic IFML are compared for their expressive powers. We introduce a logic IFML c having a non-standard syntax and a compositional semantics; in terms of this logic a syntactic fragment of IFML ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
- International Institute for Software Technology of the United Nations University: International Institute for Software Technology of the United Nations University
- Vietnam Academy of Science and Techn.: Vietnam Academy of Science and Technology
- Vietnam National Univ.: Vietnam National University
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 17 October 2005
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 30 Dec 2024
Other Metrics
Citations
Cited By
View all- El-Qurna JYahyaoui HAlmulla M(2017)A new framework for the verification of service trust behaviorsKnowledge-Based Systems10.1016/j.knosys.2017.01.011121:C(7-22)Online publication date: 1-Apr-2017