Edinburgh Research Explorer

Initial Algebras and Final Coalgebras Consisting of Nondeterministic Finite Trace Strategies

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions



  • Download as Adobe PDF

    Final published version, 316 KB, PDF document

    Licence: Creative Commons: Attribution (CC-BY)

Original languageEnglish
Pages (from-to)23-44
Number of pages22
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 11 Dec 2018


We study programs that perform I/O and finite or countable nondeterministic choice, up to finite trace equivalence. For well-founded programs, we characterize which strategies (sets of traces) are definable, and axiomatize trace equivalence by means of commutativity between I/O and nondeterminism. This gives the set of strategies as an initial algebra for a polynomial endofunctor on semilattices. The strategies corresponding to non-well-founded programs constitute a final coalgebra for this functor.

Download statistics

No data available

ID: 78364472