Abstrakt. I klassisk logik uttrycker existentiella och universella kvantifierare att det finns minst en individ som tillfredsställer en formel, eller att alla individer uppfyller en formel. I många logiker, dessa kvantifiers har generaliserats för att uttrycka att, för en icke-negativa heltal §, åtminstone § individer eller alla utom § individer uppfyller en formel. I modala logiker, graderade modaliteter generalisera standardexistentiella och universella modaliteter genom att de uttrycker, t.ex., att det finns åtminstone § tillgängliga världar som uppfyller en viss formel. Graderade metoder är användbara expressiva medel i kunskapsrepresentation; de förekommer i en mängd andra kunskapsrepresentation formalismer nära relaterade till modal logik. En naturlig fråga som uppstår är hur generaliseringen av de existentiella och universella modaliteterna påverkar decisionability-problemet för logiken och dess beräkningskomplexitet, särskilt när talen i de graderade modaliteterna kodas i binärt. I det här dokumentet studerar vi de graderade -calculus, som extenserar graderad modal logik med fasta punkter operatörer, eller, på motsvarande sätt, utvidgar klassiska -calculus med graderade metoder. Vi bevisar att decidability problem för graderade.-calculus är EXPTIME-fullständig - inte svårare än decidability problem för.-kalculus, även när siffrorna i de graderade villkoren kodas i binära.
Kupferman, Sattler och Vardi studera en μ-kalculus med graderade metoder där man kan uttrycka, t.ex., att en graf nod har minst n efterträdare som uppfyller en viss egenskap REF.
The Complexity of the Graded µ-Calculus
{'venue': 'CADE', 'journal': None, 'mag_field_of_study': ['Mathematics', 'Computer Science']}