On probabilistic state space abstraction of deterministic switched systems

This paper considers the problem of controlling the complexity of the state space abstraction of a deterministic switched affine system, which must satisfy a rich specification, expressed as an Linear Temporal Logic (LTL) formula. We propose a probabilistic approach to the state space abstraction problem that enables a trade-off between complexity and accuracy of the abstraction. Instead of a deterministic finite transition system (DFTS), the state space is abstracted to a Discrete Time Markov Chain (DTMC) using a regular state space partition. The transition relations between the discrete states and the corresponding probabilities are computed based on the Chebyshev radius of the intersection between one-step reachable sets and discrete states. The resulting abstraction is complete, but not minimal, i.e., it introduces some false transitions. In order to refine the abstraction, Monte Carlo Simulation is used, which yields a confidence measure for every transition, besides the assigned probability. Given the product automaton (PA) between the DTMC and Büchi Automaton (BA) associated with the LTL formula, a (optimal) path generation algorithm and a controller synthesis algorithm complete the proposed solution. The application of the developed methodology to a benchmark case study from the literature, i.e., airplane fuel balancing, demonstrates the effectiveness of the approach.