DROPS

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/LIPIcs.CONCUR.2016.24

Coalgebraic Trace Semantics for Buechi and Parity Automata

Authors: Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract

Despite its success in producing numerous general results on state-based dynamics, the theory of coalgebra has struggled to accommodate the Buechi acceptance condition---a basic notion in the theory of automata for infinite words or trees. In this paper we present a clean answer to the question that builds on the "maximality" characterization of infinite traces (by Jacobs and Cirstea): the accepted language of a Buechi automaton is characterized by two commuting diagrams, one for a least homomorphism and the other for a greatest, much like in a system of (least and greatest) fixed-point equations. This characterization works uniformly for the nondeterministic branching and the probabilistic one; and for words and trees alike. We present our results in terms of the parity acceptance condition that generalizes Buechi's.

Cite as

Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic Trace Semantics for Buechi and Parity Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{urabe_et_al:LIPIcs.CONCUR.2016.24,
  author =	{Urabe, Natsuki and Shimizu, Shunsuke and Hasuo, Ichiro},
  title =	{{Coalgebraic Trace Semantics for Buechi and Parity Automata}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.24},
  URN =		{urn:nbn:de:0030-drops-61867},
  doi =		{10.4230/LIPIcs.CONCUR.2016.24},
  annote =	{Keywords: coalgebra, Buechi automaton, parity automaton, probabilistic automaton, tree automaton}
}

Search Results

Documents authored by Shimizu, Shunsuke

Parity Automata for Quantitative Linear Time Logics

Abstract

Cite as

Coalgebraic Trace Semantics for Buechi and Parity Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message