An Infinitary Treatment of Full Mu-Calculus

Afshari, Bahareh; Jäger, Gerhard Max; Leigh, Graham E. (July 2019). An Infinitary Treatment of Full Mu-Calculus. Lecture notes in computer science, 11541, pp. 17-34. Springer 10.1007/978-3-662-59533-6_2

[img] Text
Jconverse.pdf - Accepted Version
Restricted to registered users only until 10 June 2020.
Available under License Publisher holds Copyright.

Download (429kB) | Request a copy
[img] Text
Afshari2019_Chapter_AnInfinitaryTreatmentOfFullMu-.pdf - Published Version
Restricted to registered users only
Available under License Publisher holds Copyright.

Download (465kB) | Request a copy

We explore the proof theory of the modal μ-calculus with converse, aka the ‘full μ-calculus’. Building on nested sequent calculi for tense logics and infinitary proof theory of fixed point logics, a cut-free sound and complete proof system for full μ-calculus is proposed. As a corollary of our framework, we also obtain a direct proof of the regular model property for the logic: every satisfiable formula has a tree model with finitely many distinct subtrees. To obtain the results we appeal to the basic theory of well-quasi-orderings in the spirit of Kozen’s proof of the finite model property for μ-calculus without converse.

Item Type:

Conference or Workshop Item (Paper)

Division/Institute:

08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG)
08 Faculty of Science > Institute of Computer Science (INF)

UniBE Contributor:

Jäger, Gerhard Max

Subjects:

000 Computer science, knowledge & systems
500 Science > 510 Mathematics

ISSN:

0302-9743

ISBN:

978-3-662-59533-6

Publisher:

Springer

Language:

English

Submitter:

Nenad Savic

Date Deposited:

21 Oct 2019 09:23

Last Modified:

24 Oct 2019 08:06

Publisher DOI:

10.1007/978-3-662-59533-6_2

BORIS DOI:

10.7892/boris.133941

URI:

https://boris.unibe.ch/id/eprint/133941

Actions (login required)

Edit item Edit item
Provide Feedback