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
|
Text
Jconverse.pdf - Accepted Version Available under License Publisher holds Copyright. Download (429kB) | Preview |
|
![[img]](https://boris.unibe.ch/style/images/fileicons/text.png) |
Text
Afshari2019_Chapter_AnInfinitaryTreatmentOfFullMu-.pdf - Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (465kB) |
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: |
05 Dec 2022 15:31 |
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 |