Search Results

Documents authored by Kozen, Dexter

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.136
Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity

Authors: Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in O(n³ log n) time via a generic partition refinement algorithm.
Cite as

Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 136:1-136:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{rozowski_et_al:LIPIcs.ICALP.2023.136,
  author =	{R\'{o}\.{z}owski, Wojciech and Kapp\'{e}, Tobias and Kozen, Dexter and Schmid, Todd and Silva, Alexandra},
  title =	{{Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{136:1--136:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.136},
  URN =		{urn:nbn:de:0030-drops-181880},
  doi =		{10.4230/LIPIcs.ICALP.2023.136},
  annote =	{Keywords: Kleene Algebra with Tests, program equivalence, completeness, coalgebra}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.142
Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness

Authors: Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety of automata corresponding to these behaviors. Finally, we prove that the axioms of the reduced fragment are sound and complete w.r.t. the semantics, and then build on this result to recover a semantics that is sound and complete w.r.t. the full set of axioms.
Cite as

Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 142:1-142:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{schmid_et_al:LIPIcs.ICALP.2021.142,
  author =	{Schmid, Todd and Kapp\'{e}, Tobias and Kozen, Dexter and Silva, Alexandra},
  title =	{{Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{142:1--142:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.142},
  URN =		{urn:nbn:de:0030-drops-142118},
  doi =		{10.4230/LIPIcs.ICALP.2021.142},
  annote =	{Keywords: Kleene algebra, program equivalence, completeness, coequations}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.1
The Ackermann Award 2018

Authors: Dexter Kozen and Thomas Schwentick

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2018 edition of the award.
Cite as

Dexter Kozen and Thomas Schwentick. The Ackermann Award 2018. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kozen_et_al:LIPIcs.CSL.2018.1,
  author =	{Kozen, Dexter and Schwentick, Thomas},
  title =	{{The Ackermann Award 2018}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{1:1--1:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.1},
  URN =		{urn:nbn:de:0030-drops-96686},
  doi =		{10.4230/LIPIcs.CSL.2018.1},
  annote =	{Keywords: Ackermann Award}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.xv
The Ackermann Award 2015

Authors: Anuj Dawar, Dexter Kozen, and Simona Ronchi Della Rocca

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
The eleventh Ackermann Award is presented at CSL'15 in Berlin, Germany. This year, again, the EACSL Ackermann Award is generously sponsored by the Kurt Gödel Society. Besides providing financial support for the Ackermann Award, the Kurt Gödel Society has also committed to inviting the recipients of the Award for a special lecture to be given to the Society in Vienna.
Cite as

Anuj Dawar, Dexter Kozen, and Simona Ronchi Della Rocca. The Ackermann Award 2015. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 15-18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.CSL.2015.xv,
  author =	{Dawar, Anuj and Kozen, Dexter and Ronchi Della Rocca, Simona},
  title =	{{The Ackermann Award 2015}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{15--18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.xv},
  URN =		{urn:nbn:de:0030-drops-54470},
  doi =		{10.4230/LIPIcs.CSL.2015.xv},
  annote =	{Keywords: Ackermann Award}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.415
Kleene Algebra with Products and Iteration Theories

Authors: Dexter Kozen and Konstantinos Mamouras

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
We develop a typed equational system that subsumes both iteration theories and typed Kleene algebra in a common framework. Our approach is based on cartesian categories endowed with commutative strong monads to handle nondeterminism.
Cite as

Dexter Kozen and Konstantinos Mamouras. Kleene Algebra with Products and Iteration Theories. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 415-431, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{kozen_et_al:LIPIcs.CSL.2013.415,
  author =	{Kozen, Dexter and Mamouras, Konstantinos},
  title =	{{Kleene Algebra with Products and Iteration Theories}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{415--431},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.415},
  URN =		{urn:nbn:de:0030-drops-42111},
  doi =		{10.4230/LIPIcs.CSL.2013.415},
  annote =	{Keywords: Kleene algebra, typed Kleene algebra, iteration theories}
}
Document
DOI: 10.4230/DagSemRep.298
Applications of Kleene Algebra (Dagstuhl Seminar 01081)

Authors: Roland C. Backhouse, Dexter Kozen, and Bernhard Möller

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Roland C. Backhouse, Dexter Kozen, and Bernhard Möller. Applications of Kleene Algebra (Dagstuhl Seminar 01081). Dagstuhl Seminar Report 298, pp. 1-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2002)

Copy BibTex To Clipboard

@TechReport{backhouse_et_al:DagSemRep.298,
  author =	{Backhouse, Roland C. and Kozen, Dexter and M\"{o}ller, Bernhard},
  title =	{{Applications of Kleene Algebra (Dagstuhl Seminar 01081)}},
  pages =	{1--21},
  ISSN =	{1619-0203},
  year =	{2002},
  type = 	{Dagstuhl Seminar Report},
  number =	{298},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.298},
  URN =		{urn:nbn:de:0030-drops-151829},
  doi =		{10.4230/DagSemRep.298},
}
Document
DOI: 10.4230/DagSemRep.193
Applications of Tree Automata in Rewriting, Logic and Programming (Dagstuhl Seminar 9743)

Authors: Hubert Comon, Dexter Kozen, Helmut Seidl, and Mosche Y. Vardi

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Hubert Comon, Dexter Kozen, Helmut Seidl, and Mosche Y. Vardi. Applications of Tree Automata in Rewriting, Logic and Programming (Dagstuhl Seminar 9743). Dagstuhl Seminar Report 193, pp. 1-34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1997)

Copy BibTex To Clipboard

@TechReport{comon_et_al:DagSemRep.193,
  author =	{Comon, Hubert and Kozen, Dexter and Seidl, Helmut and Vardi, Mosche Y.},
  title =	{{Applications of Tree Automata in Rewriting, Logic and Programming (Dagstuhl Seminar 9743)}},
  pages =	{1--34},
  ISSN =	{1619-0203},
  year =	{1997},
  type = 	{Dagstuhl Seminar Report},
  number =	{193},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.193},
  URN =		{urn:nbn:de:0030-drops-150792},
  doi =		{10.4230/DagSemRep.193},
}
Document
DOI: 10.4230/DagSemRep.41
Algebraic Complexity and Parallelism (Dagstuhl Seminar 9230)

Authors: Joachim von zur Gathen, Marek Karpinski, and Dexter Kozen

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Joachim von zur Gathen, Marek Karpinski, and Dexter Kozen. Algebraic Complexity and Parallelism (Dagstuhl Seminar 9230). Dagstuhl Seminar Report 41, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1992)

Copy BibTex To Clipboard

@TechReport{vonzurgathen_et_al:DagSemRep.41,
  author =	{von zur Gathen, Joachim and Karpinski, Marek and Kozen, Dexter},
  title =	{{Algebraic Complexity and Parallelism (Dagstuhl Seminar 9230)}},
  pages =	{1--16},
  ISSN =	{1619-0203},
  year =	{1992},
  type = 	{Dagstuhl Seminar Report},
  number =	{41},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.41},
  URN =		{urn:nbn:de:0030-drops-149291},
  doi =		{10.4230/DagSemRep.41},
}
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 About DROPS Imprint Privacy Contact