University of Leicester
Browse
main.pdf (1.23 MB)

Reactive synthesis with maximum realizability of linear temporal logic specifications

Download (1.23 MB)
journal contribution
posted on 2020-03-03, 15:59 authored by Rayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu
A challenging problem for autonomous systems is to synthesize a reactive controller that conforms to a set of given correctness properties. Linear temporal logic (LTL) provides a formal language to specify the desired behavioral properties of systems. In applications in which the specifications originate from various aspects of the system design, or consist of a large set of formulas, the overall system specification may be unrealizable. Driven by this fact, we develop an optimization variant of synthesis from LTL formulas, where the goal is to design a controller that satisfies a set of hard specifications and minimally violates a set of soft specifications. To that end, we introduce a value function that, by exploiting the LTL semantics, quantifies the level of violation of properties. Inspired by the idea of bounded synthesis, we fix a bound on the implementation size and search for an implementation that is optimal with respect to the said value function. We propose a novel maximum satisfiability encoding of the search for an optimal implementation (within the given bound on the implementation size). We iteratively increase the bound on the implementation size until a termination criterion, such as a threshold over the value function, is met.

Funding

UTC 17-S8401-10-C1

FA8650-15-C-2546

Correct-By-Construction Autonomy Protocols for Open, Reconfigurable Shipboard Networks

United States Department of the Navy

Find out more...

History

Citation

Dimitrova, R., Ghasemi, M. & Topcu, U. Reactive synthesis with maximum realizability of linear temporal logic specifications. Acta Informatica (2019).

Author affiliation

Department of Informatics

Version

  • AM (Accepted Manuscript)

Published in

ACTA INFORMATICA

Pagination

(29)

Publisher

SPRINGER

issn

0001-5903

eissn

1432-0525

Acceptance date

2019-10-25

Copyright date

2019

Available date

2019-11-09

Publisher version

https://link.springer.com/article/10.1007/s00236-019-00348-4

Language

English

Usage metrics

    University of Leicester Publications

    Categories

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC