ﻻ يوجد ملخص باللغة العربية
Reactive synthesis is a key technique for the design of correct-by-construction systems and has been thoroughly investigated in the last decades. It consists in the synthesis of a controller that reacts to environments inputs satisfying a given temporal logic specification. Common approaches are based on the explicit construction of automata and on their determinization, which limit their scalability. In this paper, we introduce a new fragment of Linear Temporal Logic, called Extended Bounded Response LTL (LTLEBR), that allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases), and we show that reactive synthesis from LTLEBR specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification. We prove the correctness of the proposed approach and we successfully evaluate it on various benchmarks.
The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption of the classic automata-theoretic approach to LTL synthesis, implemented
This paper studies the controller synthesis problem for Linear Temporal Logic (LTL) specifications using (constrained) zonotope techniques. To begin with, we implement (constrained) zonotope techniques to partition the state space and further to veri
In program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if it is too weak, the synthesised program might not match the users inte
We present a comprehensive language theoretic causality analysis framework for explaining safety property violations in the setting of concurrent reactive systems. Our framework allows us to uniformly express a number of causality notions studied in
The determinization of Buchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by McNaughton, Safra, Piterman, Sc