Skip to main content
Top
Published in:

09-11-2019 | Original Article

Reactive synthesis with maximum realizability of linear temporal logic specifications

Authors: Rayna Dimitrova, Mahsa Ghasemi, Ufuk Topcu

Published in: Acta Informatica | Issue 1-2/2020

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Business + Economics & Engineering + Technology"

Online-Abonnement

Springer Professional "Business + Economics & Engineering + Technology" gives you access to:

  • more than 102.000 books
  • more than 537 journals

from the following subject areas:

  • Automotive
  • Construction + Real Estate
  • Business IT + Informatics
  • Electrical Engineering + Electronics
  • Energy + Sustainability
  • Finance + Banking
  • Management + Leadership
  • Marketing + Sales
  • Mechanical Engineering + Materials
  • Insurance + Risk


Secure your knowledge advantage now!

Springer Professional "Business + Economics"

Online-Abonnement

Springer Professional "Business + Economics" gives you access to:

  • more than 67.000 books
  • more than 340 journals

from the following specialised fileds:

  • Construction + Real Estate
  • Business IT + Informatics
  • Finance + Banking
  • Management + Leadership
  • Marketing + Sales
  • Insurance + Risk



Secure your knowledge advantage now!

Springer Professional "Engineering + Technology"

Online-Abonnement

Springer Professional "Engineering + Technology" gives you access to:

  • more than 67.000 books
  • more than 390 journals

from the following specialised fileds:

  • Automotive
  • Business IT + Informatics
  • Construction + Real Estate
  • Electrical Engineering + Electronics
  • Energy + Sustainability
  • Mechanical Engineering + Materials





 

Secure your knowledge advantage now!

Footnotes
This content is only visible if you are logged in and have the appropriate permissions.
Literature
This content is only visible if you are logged in and have the appropriate permissions.
Metadata
Title
Reactive synthesis with maximum realizability of linear temporal logic specifications
Authors
Rayna Dimitrova
Mahsa Ghasemi
Ufuk Topcu
Publication date
09-11-2019
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 1-2/2020
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-019-00348-4

Premium Partner