Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic

Etienne Lozes

Résumé

Polyadic Higher-Order Fixpoint Logic (PHFL) is a modal fixpoint logic obtained as the merger of Higher-Order Fixpoint Logic (HFL) and the Polyadic μ-Calculus. Polyadicity enables formulas to make assertions about tuples of states rather than states only. Like HFL, PHFL has the ability to formalise properties using higher-order functions. We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of higher-order is exactly the Polyadic μ-Calculus, and it is known from Otto’s Theorem that it captures the bisimulation-invariant fragment of PTIME. We extend this and give capturing results for the bisimulation-invariant fragments of EXPTIME, PSPACE, and NLOGSPACE.
Fichier principal
Vignette du fichier
978-3-662-44602-7_8_Chapter.pdf (364.18 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01402031 , version 1 (24-11-2016)

Licence

Paternité

Identifiants

Citer

Martin Lange, Etienne Lozes. Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic. 8th IFIP International Conference on Theoretical Computer Science (TCS), Sep 2014, Rome, Italy. pp.90-103, ⟨10.1007/978-3-662-44602-7_8⟩. ⟨hal-01402031⟩
36 Consultations
45 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More