2026-07-22T10:56:55Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22787 2025-10-02T11:31:56Z ddc:004 open_access

A Complete Inference System for Probabilistic Infinite Trace Equivalence Cîrstea, Corina Moss, Lawrence S. Noquez, Victoria Schmid, Todd Silva, Alexandra Sokolova, Ana Coalgebra infinite trace semantics logic convex sets We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Corina Cîrstea and Lawrence S. Moss and Victoria Noquez and Todd Schmid and Alexandra Silva and Ana Sokolova 2025 Is Part Of LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2025.30 urn:nbn:de:0030-drops-227870 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.30 eng https://creativecommons.org/licenses/by/4.0/legalcode