Afshari, Bahareh; Jäger, Gerhard Max; Leigh, Graham E. (July 2019). An Infinitary Treatment of Full MuCalculus. Lecture notes in computer science, 11541, pp. 1734. Springer 10.1007/9783662595336_2
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 

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 cutfree 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 wellquasiorderings 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: 
03029743 
ISBN: 
9783662595336 
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/9783662595336_2 
BORIS DOI: 
10.7892/boris.133941 
URI: 
https://boris.unibe.ch/id/eprint/133941 