Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-06T08:59:58.603Z Has data issue: false hasContentIssue false
  • English
  • Français

On recursive operations over logic LTS†

Published online by Cambridge University Press:  10 November 2014

YAN ZHANG ,
ZHAOHUI ZHU  and
JINJIN ZHANG
YAN ZHANG
Affiliation:
College of Computer Science, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, P. R. China Email: [email protected], [email protected]
ZHAOHUI ZHU
Affiliation:
College of Computer Science, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, P. R. China Email: [email protected], [email protected]
JINJIN ZHANG
Affiliation:
School of Information Science, Nanjing Audit University, Nanjing 211815, P. R. China
Get access Rights & Permissions [Opens in a new window]

Abstract

Recently, in order to mix algebraic and logic styles of specification in a uniform framework, the notion of a logic labelled transition system (Logic LTS or LLTS for short) has been introduced and explored. A variety of constructors over LLTS, including usual process-algebraic operators, logic connectives (conjunction and disjunction) and standard temporal modalities (always and unless), have been given. However, no attempt has been made so far to develop the general theory concerning (nested) recursive operations over LLTS and a few fundamental problems are still open. This paper intends to study this issue in a pure process-algebraic style. A few fundamental properties, including precongruence and the uniqueness of consistent solutions of equations, will be established.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 25 , Issue 6 , September 2015 , pp. 1382 - 1431
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

This work received financial support of the National Natural Science of China (No. 60973045), Fok Ying-Tung Education Foundation, NSF of the Jiangsu Higher Education Institutions (No. 13KJB520012) and the Fundamental Research Funds for the Central Universities (No. NZ2013306).

References

Aceto, L., Ingolfsdottir, A. and Sack, J. (2012) Characteristic formulae for fixed-point semantics: A general framework. Mathematical Structures in Computer Science 22 125–173.Google Scholar
Andersen, H. R., Stirling, C. and Winskel, G. (1994) A compositional proof system for the modal μ-calculus. In: Proceeding of the 9th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press 144–153.Google Scholar
Baeten, J. C. M. and Bravetti, M. (2008) A ground-complete axiomatisation of finite-state processes in a generic process algebra. Mathematical Structures in Computer Science 18 1057–1089.Google Scholar
Bergstra, J. A., Fokkink, W. and Ponse, A. (2001) Process algebra with recursive operations. In: Bergstra, J. A., Ponse, A. and Smolka, S. A. (eds.) Handbook of Process Algebra, Elsevier Science, Chapter 5, 333–389.Google Scholar
Bergstra, J. A. and Klop, J. W. (1984) Process algebra for synchronous communication. Information and Control 60 109–137.CrossRefGoogle Scholar
Bloom, B. (1994) Ready Simulation, Bisimulation, and the Semantics of the CCS-Like Languages, Ph.D. dissertation, Massachusetts Institute of Technology, Cambridge.Google Scholar
Bloom, B., Istrail, S. and Meyer, A. R. (1995) Bisimulation can't be traced. Journal of the ACM 42 232–268.CrossRefGoogle Scholar
Bol, R. and Groote, J. F. (1996) The meaning of negative premises in transition system specifications. Journal of the ACM 43 863–914.Google Scholar
Clarke, E. M., Grumberg, O. and Peled, D. A. (2000) Model Checking, MIT Press.Google Scholar
Cleaveland, R. and Lüttgen, G. (2000) A semantic theory for heterogeneous system design. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2000). Springer-Verlag Lecture Notes in Computer Science 1974 312–324.Google Scholar
Cleaveland, R. and Lüttgen, G. (2002) A logical process calculus. In: International Workshop on Expressiveness in Concurrency (EXPRESS 2002). Electronic Notes in Theoretical Computer Science 68 (2) 33–50.Google Scholar
De Nicola, R. and Hennessy, M. (1983) Testing equivalences for processes. Theoretical Computer Science 34 83–133.Google Scholar
Groote, J. F. (1993) Transition system specifications with negative premises. Theoretical Computer Science 118 263–299.Google Scholar
Hoare, C. (1985) Communicating Sequential Processes, Prentice-Hall.Google Scholar
Larsen, K. G. and Skou, A. (2010) Bisimulation through probabilistic testing. Information and computation 94 1–28.Google Scholar
Lüttgen, G. and Vogler, W. (2007) Conjunction on processes: Full-abstraction via ready-tree semantics. Theoretical Computer Science 373 (1–2) 19–40.Google Scholar
Lüttgen, G. and Vogler, W. (2010) Ready simulation for concurrency: It is logical. Information and computation 208 845–867.Google Scholar
Lüttgen, G. and Vogler, W. (2011) Safe reasoning with Logic LTS. Theoretical Computer Science 412 3337–3357.Google Scholar
Milner, R. (1983) Calculi for synchrony and asynchrony. Theoretical Computer Science 25 (3) 267–310.Google Scholar
Milner, R. (1989a) Communication and Concurrency, Prentice-Hall.Google Scholar
Milner, R. (1989b) A complete axiomatization for observational congruence of finite-state behaviours. Information and Computation 81 227–247.CrossRefGoogle Scholar
Milner, R., Parrow, J. and Walker, D. (1992) A calculus of mobile processes, Part I/II. Information and Computation 100 1–77.CrossRefGoogle Scholar
Peled, D. A. (2001) Software Reliability Methods, Springer-Verlag.CrossRefGoogle Scholar
Pnueli, A. (1977) The temporal logic of programs. In: Symposium on Foundations of Computer Science (FOCS 1977), IEEE Computer Society Press 46–57.Google Scholar
Zhang, Y., Zhu, Z. H., Zhang, J. J. and Zhou, Y. (2011) A process algebra with logical operators. arXiv:1212.2257.Google Scholar
Zhang, Y., Zhu, Z. H. and Zhang, J. J. (2013) On recursive operations over Logic LTS. arXiv:1301.3350.Google Scholar