Search Results

Documents authored by Pattinson, Dirk

Document
DOI: 10.4230/LIPIcs.CSL.2021.26
The Alternating-Time μ-Calculus with Disjunctive Explicit Strategies

Authors: Merlin Göttlinger, Lutz Schröder, and Dirk Pattinson

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Alternating-time temporal logic (ATL) and its extensions, including the alternating-time µ-calculus (AMC), serve the specification of the strategic abilities of coalitions of agents in concurrent game structures. The key ingredient of the logic are path quantifiers specifying that some coalition of agents has a joint strategy to enforce a given goal. This basic setup has been extended to let some of the agents (revocably) commit to using certain named strategies, as in ATL with explicit strategies (ATLES). In the present work, we extend ATLES with fixpoint operators and strategy disjunction, arriving at the alternating-time µ-calculus with disjunctive explicit strategies (AMCDES), which allows for a more flexible formulation of temporal properties (e.g. fairness) and, through strategy disjunction, a form of controlled non-determinism in commitments. Our main result is an ExpTime upper bound for satisfiability checking (which is thus ExpTime-complete). We also prove upper bounds QP (quasipolynomial time) and NP∩coNP for model checking under fixed interpretations of explicit strategies, and NP under open interpretation. Our key technical tool is a treatment of the AMCDES within the generic framework of coalgebraic logic, which in particular reduces the analysis of most reasoning tasks to the treatment of a very simple one-step logic featuring only propositional operators and next-step operators without nesting; we give a new model construction principle for this one-step logic that relies on a set-valued variant of first-order resolution.
Cite as

Merlin Göttlinger, Lutz Schröder, and Dirk Pattinson. The Alternating-Time μ-Calculus with Disjunctive Explicit Strategies. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{gottlinger_et_al:LIPIcs.CSL.2021.26,
  author =	{G\"{o}ttlinger, Merlin and Schr\"{o}der, Lutz and Pattinson, Dirk},
  title =	{{The Alternating-Time \mu-Calculus with Disjunctive Explicit Strategies}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.26},
  URN =		{urn:nbn:de:0030-drops-134605},
  doi =		{10.4230/LIPIcs.CSL.2021.26},
  annote =	{Keywords: Alternating-time logic, multi-agent systems, coalitional strength}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.21
Uniform Interpolation in Coalgebraic Modal Logic

Authors: Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula - the interpolant - to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularization of logical theories. We study interpolation in the context of coalgebraic modal logics, i.e. modal logics axiomatized in rank 1, restricting for clarity to the case with finitely many modalities. Examples of such logics include the modal logics K and KD, neighbourhood logic and its monotone variant, finite-monoid-weighted logics, and coalition logic. We introduce a notion of one-step (uniform) interpolation, which refers only to a restricted logic without nesting of modalities, and show that a coalgebraic modal logic has uniform interpolation if it has one-step interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for one-step interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above.
Cite as

Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson. Uniform Interpolation in Coalgebraic Modal Logic. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{seifan_et_al:LIPIcs.CALCO.2017.21,
  author =	{Seifan, Fatemeh and Schr\"{o}der, Lutz and Pattinson, Dirk},
  title =	{{Uniform Interpolation in Coalgebraic Modal Logic}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.21},
  URN =		{urn:nbn:de:0030-drops-80415},
  doi =		{10.4230/LIPIcs.CALCO.2017.21},
  annote =	{Keywords: modal logic, coalgebraic logic, uniform interpolation, preservation of weak pullbacks}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.253
Generic Trace Semantics and Graded Monads

Authors: Stefan Milius, Dirk Pattinson, and Lutz Schröder

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
Models of concurrent systems employ a wide variety of semantics inducing various notions of process equivalence, ranging from linear-time semantics such as trace equivalence to branching-time semantics such as strong bisimilarity. Many of these generalize to system types beyond standard transition systems, featuring, for example, weighted, probabilistic, or game-based transitions; this motivates the search for suitable coalgebraic abstractions of process equivalence that cover these orthogonal dimensions of generality, i.e. are generic both in the system type and in the notion of system equivalence. In recent joint work with Kurz, we have proposed a parametrization of system equivalence over an embedding of the coalgebraic type functor into a monad. In the present paper, we refine this abstraction to use graded monads, which come with a notion of depth that corresponds, e.g., to trace length or bisimulation depth. We introduce a notion of graded algebras and show how they play the role of formulas in trace logics.
Cite as

Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic Trace Semantics and Graded Monads. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 253-269, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{milius_et_al:LIPIcs.CALCO.2015.253,
  author =	{Milius, Stefan and Pattinson, Dirk and Schr\"{o}der, Lutz},
  title =	{{Generic Trace Semantics and Graded Monads}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{253--269},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.253},
  URN =		{urn:nbn:de:0030-drops-55389},
  doi =		{10.4230/LIPIcs.CALCO.2015.253},
  annote =	{Keywords: transition systems, monads, coalgebra, trace logics}
}
Document
DOI: 10.4230/LIPIcs.STACS.2010.2492
Named Models in Coalgebraic Hybrid Logic

Authors: Lutz Schröder and Dirk Pattinson

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

Abstract
Hybrid logic extends modal logic with support for reasoning about individual states, designated by so-called nominals. We study hybrid logic in the broad context of coalgebraic semantics, where Kripke frames are replaced with coalgebras for a given functor, thus covering a wide range of reasoning principles including, e.g., probabilistic, graded, default, or coalitional operators. Specifically, we establish generic criteria for a given coalgebraic hybrid logic to admit named canonical models, with ensuing completeness proofs for pure extensions on the one hand, and for an extended hybrid language with local binding on the other. We instantiate our framework with a number of examples. Notably, we prove completeness of graded hybrid logic with local binding.
Cite as

Lutz Schröder and Dirk Pattinson. Named Models in Coalgebraic Hybrid Logic. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 645-656, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{schroder_et_al:LIPIcs.STACS.2010.2492,
  author =	{Schr\"{o}der, Lutz and Pattinson, Dirk},
  title =	{{Named Models in Coalgebraic Hybrid Logic}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{645--656},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2492},
  URN =		{urn:nbn:de:0030-drops-24920},
  doi =		{10.4230/LIPIcs.STACS.2010.2492},
  annote =	{Keywords: Logic in computer science, semantics, deduction, modal logic, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.STACS.2009.1855
Strong Completeness of Coalgebraic Modal Logics

Authors: Lutz Schröder and Dirk Pattinson

Published in: LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)

Abstract
Canonical models are of central importance in modal logic, in particular as they witness strong completeness and hence compactness. While the canonical model construction is well understood for Kripke semantics, non-normal modal logics often present subtle difficulties - up to the point that canonical models may fail to exist, as is the case e.g. in most probabilistic logics. Here, we present a generic canonical model construction in the semantic framework of coalgebraic modal logic, which pinpoints coherence conditions between syntax and semantics of modal logics that guarantee strong completeness. We apply this method to reconstruct canonical model theorems that are either known or folklore, and moreover instantiate our method to obtain new strong completeness results. In particular, we prove strong completeness of graded modal logic with finite multiplicities, and of the modal logic of exact probabilities.
Cite as

Lutz Schröder and Dirk Pattinson. Strong Completeness of Coalgebraic Modal Logics. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 673-684, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{schroder_et_al:LIPIcs.STACS.2009.1855,
  author =	{Schr\"{o}der, Lutz and Pattinson, Dirk},
  title =	{{Strong Completeness of Coalgebraic Modal Logics}},
  booktitle =	{26th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{673--684},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-09-5},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{3},
  editor =	{Albers, Susanne and Marion, Jean-Yves},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1855},
  URN =		{urn:nbn:de:0030-drops-18559},
  doi =		{10.4230/LIPIcs.STACS.2009.1855},
  annote =	{Keywords: Logic in computer science, Semantics, Deduction, Modal logic, Coalgebra}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact