12 Search Results for "Cirstea, Corina"

Volume

LIPIcs, Volume 342

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

CALCO 2025, June 16-18, 2025, University of Strathclyde, UK

Editors: Corina Cîrstea and Alexander Knapp

Document
DOI: 10.4230/LIPIcs.CSL.2026.26
ε-Distance via Lévy-Prokhorov Lifting

Authors: Josée Desharnais and Ana Sokolova

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The most studied and accepted pseudometric for probabilistic processes is one based on the Kantorovich distance between distributions. It comes with many theoretical and motivating results, in particular it is the fixpoint of a given functional and defines a functor on (complete) pseudometric spaces. It is also the foundation for a categorical lifting of pseudometrics. Other notions of behavioural pseudometrics have also been proposed, one of them (ε-distance) based on ε-bisimulation. ε-Distance has the advantages that it is intuitively easy to understand, it relates systems that are conceptually close (for example, an imperfect implementation is close to its specification), and it comes equipped with a natural notion of ε-coupling. Finally, this distance is easy to compute. We show that ε-distance is also the greatest fixpoint of a functional and provides a functor. The latter is obtained by replacing the Kantorovich distance in the lifting functor with the Lévy-Prokhorov distance. In addition, we show that ε-couplings and ε-bisimulations have an appealing coalgebraic characterization.
Cite as

Josée Desharnais and Ana Sokolova. ε-Distance via Lévy-Prokhorov Lifting. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 26:1-26:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.CSL.2026.26,
  author =	{Desharnais, Jos\'{e}e and Sokolova, Ana},
  title =	{{\epsilon-Distance via L\'{e}vy-Prokhorov Lifting}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{26:1--26:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano 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.CSL.2026.26},
  URN =		{urn:nbn:de:0030-drops-254506},
  doi =		{10.4230/LIPIcs.CSL.2026.26},
  annote =	{Keywords: L\'{e}vy-Prokhorov metric, behavioural distance, epsilon-bisimulation, reactive probabilistic transition systems, discrete labelled Markov processes, coalgebraic epsilon-(bi)simulation}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.29
Parametric Iteration in Resource Theories

Authors: Alessandro Di Giorgio, Pawel Sobocinski, and Niels Voorneveld

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Many algorithms are specified with respect to a fixed but unknown parameter. Examples of this are especially common in cryptography, where protocols often feature a security parameter such as the bit length of a secret key. Our aim is to capture this phenomenon in a more abstract setting. We focus on resource theories - general calculi of processes with a string diagrammatic syntax - introducing a general parametric iteration construction. By instantiating this construction within the Markov category of probabilistic Boolean circuits and equipping it with a suitable metric, we are able to capture the notion of negligibility via asymptotic equivalence, in a compositional way. This allows us to use diagrammatic reasoning to prove simple cryptographic theorems - for instance, proving that guessing a randomly generated key has negligible success.
Cite as

Alessandro Di Giorgio, Pawel Sobocinski, and Niels Voorneveld. Parametric Iteration in Resource Theories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 29:1-29:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{digiorgio_et_al:LIPIcs.CSL.2026.29,
  author =	{Di Giorgio, Alessandro and Sobocinski, Pawel and Voorneveld, Niels},
  title =	{{Parametric Iteration in Resource Theories}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{29:1--29:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano 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.CSL.2026.29},
  URN =		{urn:nbn:de:0030-drops-254541},
  doi =		{10.4230/LIPIcs.CSL.2026.29},
  annote =	{Keywords: Markov categories, Cryptography, String diagrams, Asymptotic equivalence}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CALCO.2025
LIPIcs, Volume 342, CALCO 2025, Complete Volume

Authors: Corina Cîrstea and Alexander Knapp

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
LIPIcs, Volume 342, CALCO 2025, Complete Volume
Cite as

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 1-292, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Proceedings{cirstea_et_al:LIPIcs.CALCO.2025,
  title =	{{LIPIcs, Volume 342, CALCO 2025, Complete Volume}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{1--292},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025},
  URN =		{urn:nbn:de:0030-drops-241021},
  doi =		{10.4230/LIPIcs.CALCO.2025},
  annote =	{Keywords: LIPIcs, Volume 342, CALCO 2025, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CALCO.2025.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Corina Cîrstea and Alexander Knapp

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cirstea_et_al:LIPIcs.CALCO.2025.0,
  author =	{C\^{i}rstea, Corina and Knapp, Alexander},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.0},
  URN =		{urn:nbn:de:0030-drops-241005},
  doi =		{10.4230/LIPIcs.CALCO.2025.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.40
Identity-Preserving Lax Extensions and Where to Find Them

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems.
Cite as

Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Identity-Preserving Lax Extensions and Where to Find Them. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 40:1-40:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.STACS.2025.40,
  author =	{Goncharov, Sergey and Hofmann, Dirk and Nora, Pedro and Schr\"{o}der, Lutz and Wild, Paul},
  title =	{{Identity-Preserving Lax Extensions and Where to Find Them}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{40:1--40:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.40},
  URN =		{urn:nbn:de:0030-drops-228665},
  doi =		{10.4230/LIPIcs.STACS.2025.40},
  annote =	{Keywords: (Bi-)simulations, lax extensions, modal logics, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.28
Strong Induction Is an Up-To Technique

Authors: Filippo Bonchi, Elena Di Lavore, and Anna Ricci

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Up-to techniques are enhancements of the coinduction proof principle which, in lattice theoretic terms, is the dual of induction. What is the dual of coinduction up-to? By means of duality, we illustrate a theory of induction up-to and we observe that an elementary proof technique, commonly known as strong induction, is an instance of induction up-to. We also show that, when generalising our theory from lattices to categories, one obtains an enhancement of the induction definition principle known in the literature as comonadic recursion.
Cite as

Filippo Bonchi, Elena Di Lavore, and Anna Ricci. Strong Induction Is an Up-To Technique. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bonchi_et_al:LIPIcs.CSL.2025.28,
  author =	{Bonchi, Filippo and Di Lavore, Elena and Ricci, Anna},
  title =	{{Strong Induction Is an Up-To Technique}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.28},
  URN =		{urn:nbn:de:0030-drops-227856},
  doi =		{10.4230/LIPIcs.CSL.2025.28},
  annote =	{Keywords: Induction, Coinduction, Up-to Techniques, Induction up-to, Lattices, Algebras}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.30
A Complete Inference System for Probabilistic Infinite Trace Equivalence

Authors: Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different.
Cite as

Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova. A Complete Inference System for Probabilistic Infinite Trace Equivalence. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cirstea_et_al:LIPIcs.CSL.2025.30,
  author =	{C\^{i}rstea, Corina and Moss, Lawrence S. and Noquez, Victoria and Schmid, Todd and Silva, Alexandra and Sokolova, Ana},
  title =	{{A Complete Inference System for Probabilistic Infinite Trace Equivalence}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{30:1--30:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.30},
  URN =		{urn:nbn:de:0030-drops-227870},
  doi =		{10.4230/LIPIcs.CSL.2025.30},
  annote =	{Keywords: Coalgebra, infinite trace, semantics, logic, convex sets}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.14
Measure-Theoretic Semantics for Quantitative Parity Automata

Authors: Corina Cîrstea and Clemens Kupke

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
Quantitative parity automata (QPAs) generalise non-deterministic parity automata (NPAs) by adding weights from a certain semiring to transitions. QPAs run on infinite word/tree-like structures, modelled as coalgebras of a polynomial functor F. They can also arise as certain products between a quantitative model (with branching modelled via the same semiring of quantities, and linear behaviour described by the functor F) and an NPA (modelling a qualitative property of F-coalgebras). We build on recent work on semiring-valued measures to define a way to measure the set of paths through a quantitative branching model which satisfy a qualitative property (captured by an unambiguous NPA running on F-coalgebras). Our main result shows that the notion of extent of a QPA (which generalises non-emptiness of an NPA, and is defined as the solution of a nested system of equations) provides an equivalent characterisation of the measure of the accepting paths through the QPA. This result makes recently-developed methods for computing nested fixpoints available for model checking qualitative, linear-time properties against quantitative branching models.
Cite as

Corina Cîrstea and Clemens Kupke. Measure-Theoretic Semantics for Quantitative Parity Automata. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cirstea_et_al:LIPIcs.CSL.2023.14,
  author =	{C\^{i}rstea, Corina and Kupke, Clemens},
  title =	{{Measure-Theoretic Semantics for Quantitative Parity Automata}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{14:1--14:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.14},
  URN =		{urn:nbn:de:0030-drops-174755},
  doi =		{10.4230/LIPIcs.CSL.2023.14},
  annote =	{Keywords: parity automaton, coalgebra, measure theory}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2017.7
Parity Automata for Quantitative Linear Time Logics

Authors: Corina Cirstea, Shunsuke Shimizu, and Ichiro Hasuo

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

Abstract
We initiate a study of automata-based model checking for previously proposed quantitative linear time logics interpreted over coalgebras. Our results include: (i) an automata-theoretic characterisation of the semantics of these logics, based on a notion of extent of a quantitative parity automaton, (ii) a study of the expressive power of Buchi variants of such automata, with implications on the expressiveness of fragments of the logics considered, and (iii) a naive algorithm for computing extents, under additional assumptions on the domain of truth values.
Cite as

Corina Cirstea, Shunsuke Shimizu, and Ichiro Hasuo. Parity Automata for Quantitative Linear Time Logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cirstea_et_al:LIPIcs.CALCO.2017.7,
  author =	{Cirstea, Corina and Shimizu, Shunsuke and Hasuo, Ichiro},
  title =	{{Parity Automata for Quantitative Linear Time Logics}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{7:1--7:18},
  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.7},
  URN =		{urn:nbn:de:0030-drops-80468},
  doi =		{10.4230/LIPIcs.CALCO.2017.7},
  annote =	{Keywords: coalgebra, quantitative logic, linear time logic, parity automaton}
}
Document
DOI: 10.4230/LITES-v004-i001-a003
Quantitative Analysis of Consistency in NoSQL Key-Value Stores

Authors: Si Liu, Jatin Ganhotra, Muntasir Raihan Rahman, Son Nguyen, Indranil Gupta, and José Meseguer

Published in: LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1

Abstract
The promise of high scalability and availability has prompted many companies to replace traditional relational database management systems (RDBMS) with NoSQL key-value stores. This comes at the cost of relaxed consistency guarantees: key-value stores only guarantee eventual consistency in principle. In practice, however, many key-value stores seem to offer stronger consistency. Quantifying how well consistency properties are met is a non-trivial problem.  We address this problem by formally modeling key-value stores as probabilistic systems and quantitatively analyzing their consistency properties by both statistical model checking and implementation evaluation. We present for the first time a formal probabilistic model of Apache Cassandra, a popular NoSQL key-value store, and quantify how much Cassandra achieves various consistency guarantees under various conditions. To validate our model, we evaluate multiple consistency properties using two methods and compare them against each other. The two methods are: (1) an implementation-based evaluation of the source code; and (2) a statistical model checking analysis of our probabilistic model.
Cite as

Si Liu, Jatin Ganhotra, Muntasir Raihan Rahman, Son Nguyen, Indranil Gupta, and José Meseguer. Quantitative Analysis of Consistency in NoSQL Key-Value Stores. In LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1, pp. 03:1-03:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{liu_et_al:LITES-v004-i001-a003,
  author =	{Liu, Si and Ganhotra, Jatin and Rahman, Muntasir Raihan and Nguyen, Son and Gupta, Indranil and Meseguer, Jos\'{e}},
  title =	{{Quantitative Analysis of Consistency in NoSQL Key-Value Stores}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{03:1--03:26},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES-v004-i001-a003},
  URN =		{urn:nbn:de:0030-drops-192649},
  doi =		{10.4230/LITES-v004-i001-a003},
  annote =	{Keywords: NoSQL Key-value Store, Consistency, Statistical Model Checking, Rewriting Logic, Maude}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.66
Canonical Coalgebraic Linear Time Logics

Authors: Corina Cirstea

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

Abstract
We extend earlier work on linear time fixpoint logics for coalgebras with branching, by showing how propositional operators arising from the choice of branching monad can be canonically added to these logics. We then consider two semantics for the uniform modal fragments of such logics: the previously-proposed, step-wise semantics and a new semantics akin to those of path-based logics. We prove that the two semantics are equivalent, and show that the canonical choice made for resolving branching in these logics is crucial for this property. We also state conditions under which similar, non-canonical logics enjoy the same property - this applies both to the choice of a branching modality and to the choice of linear time modalities. Our logics allow reasoning about linear time behaviour in systems with non-deterministic, probabilistic or weighted branching. In all these cases, the logics enhanced with propositional operators gain in expressiveness. Another contribution of our work is a reformulation of fixpoint semantics, which applies to any coalgebraic modal logic whose semantics arises from a one-step semantics.
Cite as

Corina Cirstea. Canonical Coalgebraic Linear Time Logics. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 66-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{cirstea:LIPIcs.CALCO.2015.66,
  author =	{Cirstea, Corina},
  title =	{{Canonical Coalgebraic Linear Time Logics}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{66--85},
  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.66},
  URN =		{urn:nbn:de:0030-drops-55274},
  doi =		{10.4230/LIPIcs.CALCO.2015.66},
  annote =	{Keywords: coalgebra, linear time logic, fixpoint logic}
}
  • Refine by Type
  • 11 Document/PDF
  • 5 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 2 2026
  • 6 2025
  • 1 2023
  • 2 2017
  • 1 2015

  • Refine by Author
  • 4 Cîrstea, Corina
  • 2 Cirstea, Corina
  • 2 Knapp, Alexander
  • 2 Sokolova, Ana
  • 1 Bonchi, Filippo
  • Show More...

  • Refine by Series/Journal
  • 10 LIPIcs
  • 1 LITES

  • Refine by Classification
  • 3 Theory of computation → Categorical semantics
  • 3 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Algebraic semantics
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Models of computation
  • Show More...

  • Refine by Keyword
  • 4 coalgebra
  • 2 linear time logic
  • 2 parity automaton
  • 1 (Bi-)simulations
  • 1 Algebras
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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