We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

Abstract: The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of stability of chain colimits; we extend the framework to the presence of a monadic effect, too, restricting to fibrations of complete lattice-valued predicates. Practical benefits of our categorical theory are exemplified by new "upside-down" witness notions for three verification problems: probabilistic liveness, and acceptance and model-checking with respect to bottom-up tree automata.
Comments: 38 pages
Subjects: Logic in Computer Science (cs.LO); Computation and Language (cs.CL)
DOI: 10.4230/LIPIcs.CONCUR.2021.21
Cite as: arXiv:2105.04817 [cs.LO]
  (or arXiv:2105.04817v3 [cs.LO] for this version)

Submission history

From: Mayuko Kori [view email]
[v1] Tue, 11 May 2021 07:10:13 GMT (140kb,D)
[v2] Wed, 7 Jul 2021 07:11:05 GMT (144kb,D)
[v3] Tue, 24 Aug 2021 09:26:16 GMT (144kb,D)

Link back to: arXiv, form interface, contact.