We consider synthesis problems from logical specifications over infinite data domains, expressed in the logic constraint LTL (CLTL), which extends LTL with predicates over an infinite set of data values. We consider register-bounded synthesis, where the goal is to automatically generate, if it exists, a transducer with r registers that realizes a given CLTL formula, where r is also given as input. We prove that CLTL register-bounded synthesis is 2ExpTime-c for various data domains such as any infinite set with equality, (Q,<), and (N,<). For the latter domain, this contrasts with known undecidability results of (unbounded) register CLTL synthesis, by Bhaskar and Praveen. Lastly, we consider synthesis in a partial observation setting by extending CLTL with invisible variables. 2012 ACM Subject Classification Theory of computation -> Automata over infinite objects; Theory of computation -> Modal and temporal logics
Probabilistic models of computation have been studied for over three decades now, from foundational, logical, coalgebraic, categorical, as well as more practical verification-motivated point of view. In my work, and in this talk, we focus on the foundational, semantics side of probabilistic automata and transition systems, and in particular the relevant monads, and their algebras. The interplay of probability and non-determinism has been particularly challenging from a semantics point of view for some decades, as it does not just yield a monad. There are by now well-studied solutions to this and several monads for probability and non-determinism: some enriching the structure with convexity to obtain a monad, albeit a non-commutative one, others deliberately simplifying it, by imposing commutativity. It is well known that monads have two faces: a computational one - we think here of the powerset monad modelling non-determinism, or the probability distribution monad modelling probabilistic choices, and a universal-algebraic one - where we think of the algebraic presentation of the monads, like semilattices for the powerset monad and (variants of) convex algebras for (variants of) the probability distribution monad. Combining non-determinism and probability yields other combined monads, among which probably the most studied is the convex-subsets-of-distributions monad. This monad is presented by so-called convex semilattices, algebraic structures that are both a semilattice and a convex algebra, with suitable distributivity connecting the operations. From a semantics point of view, the algebraic presentations give us a nice way to define (and sometimes compute) language (aka trace) equivalence of the corresponding automata. Moreover, the presentations are useful for axiomatizations of language equivalence. From an algebraic point of view, these algebras are interesting and many questions about them are still open. We will discuss language semantics, its axiomatization, as well as some obtained and open algebraic problems for convex algebras and convex semilattices - and their computational consequences. In particular, we have a full characterization of congruences of (variants of) convex algebras, which for example yields decidability of distribution semantics; other results on congruences, e.g. a result on a congruence being finitely generated as a subalgebra, surprisingly accellerated the proof of completeness of infinite trace semanitcs, etc. We will review some existing results: all congruences are described and fp = fg for convex algebras, termination is a black hole, useful functors are proper on convex algebras, cancellativity of convex semi-lattices; as well as mention ongoing work on: mid-point-cancellativity, subalgebras, and homomorphisms for convex semi-lattices, as well as topological convex semilattices. This talk is based on previous joint works with Filippo Bonchi, Alexandra Silva, Valeria Vignudelli, and Harald Woracek, as well as on ongoing work and discussions with Matteo Mio, Alex Simpson, and Harald Woracek. 2012 ACM Subject Classification Theory of computation -> Probabilistic computation; Theory of computation -> Categorical semantics; Theory of computation -> Logic and verification; Theory of computation -> Program verification; Theory of computation -> Randomness, geometry and discrete structures
We examine how the standard proof that left adjoints preserve colimits behaves in the setting of wild categories, a natural setting for synthetic homotopy theory inside homotopy type theory. We prove that the proof may fail for adjunctions between wild categories. Our core contribution, however, is a sufficient condition on the left adjoint for the proof to go through. The condition, called 2-coherence, expresses that the naturality structure of the hom-isomorphism commutes with composition of morphisms. We present two useful examples of this condition in action. First, we use it, along with a new version of a known trick for homogeneous types, to show that the suspension functor preserves graph-indexed colimits. Second, we show that every modality, viewed as a functor on coslices of a type universe, is 2-coherent as a left adjoint to the forgetful functor from the subcategory of modal types, thereby proving this subcategory is cocomplete. We have formalized our main results in Agda. 2012 ACM Subject Classification Theory of computation -> Type theory
