Hostname: page-component-cd9895bd7-gbm5v Total loading time: 0 Render date: 2024-12-25T13:50:04.086Z Has data issue: false hasContentIssue false
  • English
  • Français

Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski

Published online by Cambridge University Press:  12 March 2014

Giovanna D'agostino  and
Marco Hollenberg
Giovanna D'agostino
Affiliation:
Illc, Universiteit van Amsterdam, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands Udine University, Department of Mathematics and Computer Science, Viale Delle Scienze 206, 33100 Udine, Italy, E-mail: [email protected]
Marco Hollenberg
Affiliation:
Utrecht University, Department of Philosophy, Heidelberglaan 8, 3584 CS Utrecht, The Netherlands, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Extract

The (modal) μ-calculus ([14]) is a very powerful extension of modal logic with least and greatest fixed point operators. It is of great interest to computer science for expressing properties of processes such as termination (every run is finite) and fairness (on every infinite run, no action is repeated infinitely often to the exclusion of all others).

The power of the μ-calculus is also evident from a more theoretical perspective. The μ-calculus is a fragment of monadic second-order logic (MSO) containing only formulae that are invariant for bisimulation, in the sense that they cannot distinguish between bisimilar states. Janin and Walukiewicz prove the converse: any property which is invariant for bisimulation and MSO-expressible is already expressible in the μ-calculus ([13]). Yet the μ-calculus enjoys many desirable properties which MSO lacks, like a complete sequent-calculus ([29]), an exponential-time decision procedure, and the finite model property ([25]). Switching from MSO to its bisimulation-invariant fragment gives us these desirable properties.

In this paper we take a classical logician's view of the μ-calculus. As far as we are concerned a new logic should not be allowed into the community of logics without at least considering the standard questions that any logic is bothered with. In this paper we perform this rite of passage for the μ-calculus. The questions we will be concerned with are the following.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 65 , Issue 1 , March 2000 , pp. 310 - 332
Copyright
Copyright © Association for Symbolic Logic 2000

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.)

References

REFERENCES

[1]Chang, C.C. and Keisler, H.J., Model theory, Studies in Logic and the Foundations of Mathematics, vol. 173, Elsevier Science Publishers B.V., 1977.Google Scholar
[2]Clarke, E.M., Emerson, E.A., and Sistla, A.P., Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol. 8(2) (1986), pp. 244–263.CrossRefGoogle Scholar
[3]Craig, W., Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, this Journal, vol. 22 (1957), pp. 269–285.Google Scholar
[4]Ebbinghaus, H. and Flum, J., Finite model theory, Springer, Berlin, 1995.Google Scholar
[5]Emerson, E.A. and Halpern, J.Y., Sometimes and not never revisited: on branching versus linear time, Journal of the ACM, vol. 33(1) (1986), pp. 151–178.CrossRefGoogle Scholar
[6]Emerson, E.A. and Lei, Chin-Laung, Modalities for model checking: branching time logic strikes back, Science of Computer Programming, vol. 8 (1987), pp. 275–306.CrossRefGoogle Scholar
[7]Fisher, M.J. and Ladner, R.E., Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol. 18(2) (1979), pp. 194–211.CrossRefGoogle Scholar
[8]Gurevich, Y., Towards logic tailored for logical complexity, Computation and proof theory (Richter, M. M.et al., editors), Lecture Notes in Mathematics, vol. 1104, Springer, 1984, pp. 175–216.CrossRefGoogle Scholar
[9]Henkin, L., An extension of the Craig-Lyndon interpolation theorem, this Journal, vol. 28 (1963), pp. 201–216.Google Scholar
[10]Hodges, W., Model theory, Encyclopedia of Mathematics and Its Applications, vol. 42, Cambridge University Press, 1993.CrossRefGoogle Scholar
[11]Janin, D., Propriétés logiques du nondéterminisme et μ-calcul modal, Ph.D. thesis, LaBRI–Université de Bordeaux I, 1996.Google Scholar
[12]Janin, D. and Walukiewicz, I., Automata for the modal μ-calculus and related results, Proceedings MFCS'95, Springer, 1995, pp. 552–562.Google Scholar
[13]Janin, D., On the expressive completeness of the propositional μ-calculus w. r. t. monadic second-order logic, to appear in the Proceedings of CONCUR'96, 1996.CrossRefGoogle Scholar
[14]Kozen, D., Results on the propositional μ-calculus, Theoretical Computer Science, vol. 27 (1983), pp. 234–241.CrossRefGoogle Scholar
[15]Łos, J., On the extending of models (I), Fundamentae Mathematicae, vol. 42 (1955), pp. 38–54.CrossRefGoogle Scholar
[16]Lyndon, R.C., An interpolation theorem in the predicate calculus, Pacific Journal of Mathematics, vol. 9 (1959), pp. 155–164.CrossRefGoogle Scholar
[17]Maksimova, L., Absence of interpolation and of Beth's property in temporal logics with “the next” operation, Siberian Mathematical Journal, vol. 32(6) (1991), pp. 109–113.Google Scholar
[18]Maksimova, L., Temporal logics of “the next” do not have the Beth property, Journal of applied nonclassical logics, vol. 1(1) (1991), pp. 73–76.CrossRefGoogle Scholar
[19]Niwiński, D., Fixed points vs. infinite generation, Proceedings of the 3rd Annual IEEE Symposium on Logic in Computer Science, 1988, pp. 402–409.Google Scholar
[20]Pitts, A., On an interpretation of second-order quantification in first-order intuitionistic propositional logic, this Journal, vol. 57 (1992), pp. 33–52.Google Scholar
[21]Pnueli, A., The temporal logic of programs, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46–57.Google Scholar
[22]Pratt, V., Semantical considerations on Floyd-Hoare logic, Proceedings of the 17th IEEE Symposium on Foundations of Computer Science, 1976, pp. 109–121.Google Scholar
[23]de Ruke, M., Extending modal logic, Ph.D. thesis, ILLC-dissertation series 1993-4, 1993.Google Scholar
[24]de Ruke, M., Modal model theory, Annals of Pure and Applied Logic (1997), to appear.Google Scholar
[25]Streett, R.S. and Emerson, E.A., An automata theoretic procedure for the propositional mucalculus, Information and Computation, vol. 81 (1989), pp. 249–264.CrossRefGoogle Scholar
[26]Tarski, A., Contributions to the theory of models I, II, Indagationes Mathematicae, vol. 16 (1954), pp. 572–588.CrossRefGoogle Scholar
[27]Thomas, W., Automata on infinite objects, Handbook of theoretical computer science, volume B (Leeuwen, J. van, editor), Elsevier, 1990, pp. 133–191.Google Scholar
[28]Visser, A., Bisimulations, model descriptions and propositional quantifiers, Logic Group Preprint Series, vol. 161, Department of Philosophy, Utrecht University, 1996.Google Scholar
[29]Walukiewicz, I., Completeness of Kozen's axiomatization of the propositional μ-calculus, Proceedings LICS'95, 1995, pp. 14–24.Google Scholar