License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2015.320
URN: urn:nbn:de:0030-drops-55424
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5542/
Go to the corresponding LIPIcs Volume Portal

Urabe, Natsuki ; Hasuo, Ichiro

Coalgebraic Infinite Traces and Kleisli Simulations

pdf-format:
22.pdf (0.5 MB)

Abstract

Kleisli simulation is a categorical notion introduced by Hasuo to verify finite trace inclusion. They allow us to give definitions of forward and backward simulation for various types of systems. A generic categorical theory behind Kleisli simulation has been developed and it guarantees the soundness of those simulations wrt. finite trace semantics. Moreover, those simulations can be aided by forward partial execution (FPE) - a categorical transformation of systems previously introduced by the authors.

In this paper, we give Kleisli simulation a theoretical foundation that assures its soundness also wrt. infinite trace. There, following Jacobs' work, infinite trace semantics is characterized as the "largest homomorphism." It turns out that soundness of forward simulations is rather straightforward; that of backward simulation holds too, although it requires certain additional conditions and its proof is more involved. We also show that FPE can be successfully employed in the infinite trace setting to enhance the applicability of Kleisli simulations as witnesses of trace inclusion. Our framework is parameterized in the monad for branching as well as in the functor for linear-time behaviors; for the former we use the powerset monad (for nondeterminism) as well as the sub-Giry monad (for probability).

BibTeX - Entry

@InProceedings{urabe_et_al:LIPIcs:2015:5542,
  author =	{Natsuki Urabe and Ichiro Hasuo},
  title =	{{Coalgebraic Infinite Traces and Kleisli Simulations}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{320--335},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Lawrence S. Moss and Pawel Sobocinski},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5542},
  URN =		{urn:nbn:de:0030-drops-55424},
  doi =		{10.4230/LIPIcs.CALCO.2015.320},
  annote =	{Keywords: category theory, coalgebra, simulation, verification, trace semantics}
}

Keywords: category theory, coalgebra, simulation, verification, trace semantics
Collection: 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)
Issue Date: 2015
Date of publication: 28.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI