Source author record

Cătălin Dima

Cătălin Dima appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Logic in Computer Science Multiagent Systems

Catalog footprint

What is connected

3works

2topics

4close collaborators

Actions

Connect this record

Open graph Browse works

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

preprint2014arXiv

The Expressive Power of Epistemic $μ$-Calculus

While the $μ$-calculus notoriously subsumes Alternating-time Temporal Logic (ATL), we show that the epistemic $μ$-calculus does not subsume ATL with imperfect information (ATL$_i$) for the synchronous perfect-recall semantics. To prove this we first establish that jumping parity tree automata (JTA), a recently introduced extension of alternating parity tree automata, are expressively equivalent to the epistemic $μ$-calculus, and this for any knowledge semantics. Using this result we also show that, for bounded-memory semantics, the epistemic $μ$-calculus is not more expressive than the standard $μ$-calculus, and that its satisfiability problem is EXPTIME-complete.

preprint2012arXiv

Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics

We show that the model-checking problem is decidable for a fragment of the epistemic μ-calculus. The fragment allows free variables within the scope of epistemic modalities in a restricted form that avoids constructing formulas embodying any form of common knowledge. Our calculus subsumes known decidable fragments of epistemic CTL/LTL. Its modal variant can 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 ATL with imperfect information and perfect recall can be encoded as instances of the model-checking problem for this epistemic μ-calculus.

preprint2010arXiv

Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions

We present a variant of ATL with distributed knowledge operators based on a synchronous and perfect recall semantics. The coalition modalities in this logic are based on partial observation of the full history, and incorporate a form of cooperation between members of the coalition in which agents issue their actions based on the distributed knowledge, for that coalition, of the system history. We show that model-checking is decidable for this logic. The technique utilizes two variants of games with imperfect information and partially observable objectives, as well as a subset construction for identifying states whose histories are indistinguishable to the considered coalition.