Abstract Temporal stream logic (TSL) extends LTL with updates and predicates over arbitrary function terms. This allows for specifying data-intensive systems for which LTL is not expressive enough. In the semantics of TSL, functions and predicates are left uninterpreted. In this paper, we extend TSL with first-order theories, enabling us to specify systems using interpreted functions and predicates such as incrementation or equality. We investigate the satisfiability problem of TSL modulo the standard underlying theory of uninterpreted functions as well as with respect to Presburger arithmetic and the theory of equality: For all three theories, TSL satisfiability is neither semi-decidable nor co-semi-decidable. Nevertheless, we identify three fragments of TSL for which the satisfiability problem is (semi-)decidable in the theory of uninterpreted functions. Despite the undecidability, we present an algorithm – which is not guaranteed to terminate – for checking the satisfiability of a TSL formula in the theory of uninterpreted functions and evaluate it: It scales well and is able to validate assumptions in a real-world system design.

Reactive synthesis automatically derives a strategy that satisfies a given specification. However, requiring a strategy to meet the specification in every situation is, in many cases, too hard of a requirement. Particularly in compositional synthesis of distributed systems, individual winning strategies for the processes often do not exist. Remorsefree dominance, a weaker notion than winning, accounts for such situations: dominant strategies are only required to be as good as any alternative strategy, i.e., they are allowed to violate the specification if no other strategy would have satisfied it in the same situation. The composition of dominant strategies is only guaranteed to be dominant for safety properties, though; preventing the use of dominance in compositional synthesis for liveness specifications. Yet, safety properties are often not expressive enough. In this paper, we thus introduce a new winning condition for strategies, called delay-dominance, that overcomes this weakness of remorsefree~dominance: we show that it is compositional for many safety and liveness specifications, enabling a compositional synthesis algorithm based on delay-dominance for general specifications. Furthermore, we introduce an automaton construction for recognizing delay-dominant strategies and prove its soundness and completeness. The resulting automaton is of single-exponential size in the squared length of the specification and can immediately be used for safraless synthesis procedures. Thus, synthesis of delay-dominant strategies is, as synthesis of winning strategies, in 2EXPTIME.

We present BOCoSy, a tool for Bounded symbolic Output-feedback Controller Synthesis. Given a specification, BOCoSy synthesizes symbolic output-feedback controllers which interact with a given plant via a pre-defined finite symbolic interface. BOCoSy solves this problem by a new lazy abstraction-refinement technique which starts with a very coarse abstraction of the external trace semantics of the given plant and iteratively removes non-admissible behavior from this abstract model until a controller is found. BOCoSy steers the search for controllers towards small and concise state space representations by utilizing ideas from bounded synthesis. As a result, BOCoSy returns small and explainable controllers that are still powerful enough to solve the given synthesis problem. We show that BOCoSy is able to synthesize small, human readable symbolic controllers quickly on a set of benchmarks.