Alternating Automata and Up-To Techniques via Weak Distributive Laws

The coalgebraic determinization of alternating automata has long been obstructed by the absence of distributive law of the powerset monad over it- self [5, 6]. This can be fixed using the framework of weak distributive laws [3], as there is a unique well-behaved weak distributive law of the requested type. In our recent paper [4], we applied a similar strategy to cope with the absence of distributive law between the powerset monad and the distribu- tion monad. Here, we extend the framework of weak distributive laws to the case when one of the monads is only a functor, provide an abstract compo- sitionality result in the style of Cheng [2] and systematic soundness of up-to techniques. Along the way, we apply these results to alternating automata as a mo- tivating example. Another example is given by probabilistic automata, for which our results yield soundness of bisimulation up-to convex hull [1]. This talk is based on a submitted paper jointly written with Daniela Petrisan.

Authors

• Alexandre Goy

Keywords

No keywords are indexed for this paper.