2019/10/04 by Rayna Dimitrova, Mahsa Ghasemi, Dimitrova, Rayna +3
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques
paper · pdf · doi:10.48550/arxiv.1910.02561
A challenging problem for autonomous systems is to synthesize a reactive\ncontroller that conforms to a set of given correctness properties. Linear\ntemporal logic (LTL) provides a formal language to specify the desired\nbehavioral properties of systems. In applications in which the specifications\noriginate from various aspects of the system design, or consist of a large set\nof formulas, the overall system specification may be unrealizable. Driven by\nthis fact, we develop an optimization variant of synthesis from LTL formulas,\nwhere the goal is to design a controller that satisfies a set of hard\nspecifications and minimally violates a set of soft specifications. To that\nend, we introduce a value function that, by exploiting the LTL semantics,\nquantifies the level of violation of properties. Inspired by the idea of\nbounded synthesis, we fix a bound on the implementation size and search for an\nimplementation that is optimal with respect to the said value function. We\npropose a novel maximum satisfiability encoding of the search for an optimal\nimplementation (within the given bound on the implementation size). We\niteratively increase the bound on the implementation size until a termination\ncriterion, such as a threshold over the value function, is met.\n