Pith. sign in

REVIEW 1 cited by

Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics

Not yet reviewed by Pith; the record is open.

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1310.6434 v1 pith:MFMBXIBL submitted 2013-10-23 cs.GT cs.LO

classification cs.GTcs.LO
keywords epistemicdecidablesubproblemforminstancesmodel-checkingmu-calculusproblem
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

We identify a subproblem of the model-checking problem for the epistemic \mu-calculus which is decidable. Formulas in the instances of this subproblem allow free variables within the scope of epistemic modalities in a restricted form that avoids embodying any form of common knowledge. Our subproblem subsumes known decidable fragments of epistemic CTL/LTL, may express winning strategies in two-player games with one player having imperfect information and non-observable objectives, and, with a suitable encoding, decidable instances of the model-checking problem for ATLiR.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Dealing with imperfect information in Strategy Logic

    cs.LO 2019-08 conditional novelty 6.0 of 10

    A new Epistemic Strategy Logic internalizes uniformity and other strategy properties in the object language, and its perfect-information core BSL is shown equiexpressive with Strategy Logic.

Pith tools