Formal synthesis approaches over stochastic systems have received significant attention in the past few years, in view of their ability to provide provably correct controllers for complex logical specifications in an automated fashion. Examples of complex specifications include properties expressed as formulae in linear temporal logic (LTL) or as automata on infinite strings. A general methodology to synthesize controllers for such properties resorts to symbolic models of the given stochastic systems. Symbolic models are finite abstractions of the given concrete systems with the property that a controller designed on the abstraction can be refined (or implemented) into a controller on the original system. Although the recent development of techniques for the construction of symbolic models has been quite encouraging, the general goal of formal synthesis over stochastic control systems is by no means solved. A fundamental issue with the existing techniques is the known “curse of dimensionality,” which is due to the need to discretize state and input sets. Such discretization generally results in an exponential complexity over the number of state and input variables in the concrete system. In this work we propose a novel abstraction technique for incrementally stable stochastic control systems, which does not require state-space discretization but only input set discretization, and that can be potentially more efficient (and thus scalable) than existing approaches. We elucidate the effectiveness of the proposed approach by synthesizing a schedule for the coordination of two traffic lights under some safety and fairness requirements for a road traffic model. Further we argue that this 5-dimensional linear stochastic control system cannot be studied with existing approaches based on state-space discretization due to the very large number of generated discrete states.

@en

We consider the problem of incorporating control tasks on top of a partially loaded shared computing resource, whose current task execution pattern is characterizable using a window based pattern. We consider that the control task to be scheduled is allowed to switch between multiple controllers, each with different associated sampling rate, in order to adjust its requirement of computational bandwidth as per availability. We provide a novel control theoretic analysis that derives a Timed Automata (TA) based specification of allowable switchings among the different controller options while retaining the asymptotic stability of the closed loop. Our scheduling scheme computes a platform level residual bandwidth pattern from individual task level execution patterns. We then leverage the TA based controller specification and the residual bandwidth pattern in order to synthesize a Linearly Priced Timed Automata for which the minimum cost reachability solution provides realizable multi-rate control schedules. The provided scheduler not only guarantees the asymptotic stability of the control loop but also increases the robustness and control performance of the implementation by maximizing the bandwidth utilization.@en