Paper Info
Title
Safraless LTL synthesis considering maximal realizability.
Abstract
Linear temporal logic (LTL) synthesis is a formal method for automatically composing a reactive system that realizes a given behavioral specification described in LTL if the specification is realizable. Even if the whole specification is unrealizable, it is preferable to synthesize a best-effort reactive system. That is, a system that maximally realizes its partial specifications. Therefore, we categorized specifications into must specifications (which should never be violated) and desirable specifications (the violation of which may be unavoidable). In this paper, we propose a method for synthesizing a reactive system that realizes all must specifications and strongly endeavors to satisfy each desirable specification. The general form of the desirable specifications without assumptions is $$\mathbf{G }\varphi $$G¿, which means "$$\varphi $$¿ always holds". In our approach, the best effort to satisfy $$\mathbf{G }\varphi $$G¿ is to maximize the number of steps satisfying $$\varphi $$¿ in the interaction. To quantitatively evaluate the number of steps, we used a mean-payoff objective based on LTL formulae. Our method applies the Safraless approach to construct safety games from given must and desirable specifications, where the must specification can be written in full LTL and may include assumptions. It then transforms the safety games constructed from the desirable specifications into mean-payoff games and finally composes a reactive system as an optimal strategy on a synchronized product of the games.
Year
DOI
Venue
2017
10.1007/s00236-016-0280-3
Acta Inf.
Field
DocType
Volume
Discrete mathematics,Linear temporal logic,Formal methods,Reactive system,Mathematics,Realizability
Journal
54
Issue
ISSN
Citations 
7
1432-0525
3
PageRank 
References 
Authors
0.41
29
5
Name
Order
Citations
PageRank
Takashi Tomita191.90
Atsushi Ueno2182.33
Masaya Shimakawa3417.54
Shigeki Hagihara47812.33
Naoki Yonezaki510720.02