ML p(r)ior | A multi-paradigm language for reactive synthesis

A multi-paradigm language for reactive synthesis

2016-02-03
This paper proposes a language for describing reactive synthesis problems that integrates imperative and declarative elements. The semantics is defined in terms of two-player turn-based infinite games with full information. Currently, synthesis tools accept linear temporal logic (LTL) as input, but this description is less structured and does not facilitate the expression of sequential constraints. This motivates the use of a structured programming language to specify synthesis problems. Transition systems and guarded commands serve as imperative constructs, expressed in a syntax based on that of the modeling language Promela. The syntax allows defining which player controls data and control flow, and separating a program into assumptions and guarantees. These notions are necessary for input to game solvers. The integration of imperative and declarative paradigms allows using the paradigm that is most appropriate for expressing each requirement. The declarative part is expressed in the LTL fragment of generalized reactivity(1), which admits efficient synthesis algorithms, extended with past LTL. The implementation translates Promela to input for the Slugs synthesizer and is written in Python. The AMBA AHB bus case study is revisited and synthesized efficiently, identifying the need to reorder binary decision diagrams during strategy construction, in order to prevent the exponential blowup observed in previous work.
PDF

Highlights - Most important sentences from the article

Login to like/save this paper, take notes and configure your recommendations

Related Articles

2019-05-31

We study the reactive synthesis problem for hyperproperties given as formulas of the temporal logic … show more
PDF

Highlights - Most important sentences from the article

2019-04-14
1904.06668 | cs.SE

Spectra is a new specification language for reactive systems, specifically tailored for the context … show more
PDF

Highlights - Most important sentences from the article

2017-12-01

Reactive systems that operate in environments with complex data, such as mobile apps or embedded con… show more
PDF

Highlights - Most important sentences from the article

2019-02-14

Many problems in reactive synthesis are stated using two formulas ---an environment assumption and a… show more
PDF

Highlights - Most important sentences from the article

2018-12-01

We study model checking of client - server systems, where the servers offer several types of service… show more
PDF

Highlights - Most important sentences from the article

2019-01-14

In this paper, we propose an asynchronous distributed algorithm for the computation of generalized N… show more
PDF

Highlights - Most important sentences from the article

2018-02-21

We introduce two-player games which build words over infinite alphabets, and we study the problem of… show more
PDF

Highlights - Most important sentences from the article

2016-11-23
1611.07803 | cs.LO

This paper considers the problem of assumptions refinement in the context of unrealizable specificat… show more
PDF

Highlights - Most important sentences from the article

2019-03-29

The synthesis - the automatic construction - of reactive systems from linear temporal logic (LTL) sp… show more
PDF

Highlights - Most important sentences from the article

2018-08-31

In this paper, we investigate the problem of synthesizing strategies for linear temporal logic (LTL)… show more
PDF

Highlights - Most important sentences from the article

2018-07-24

Most algorithms for the synthesis of reactive systems focus on the construction of finite-state mach… show more
PDF

Highlights - Most important sentences from the article

2019-01-03
1901.00591 | cs.LO

In formal synthesis of reactive systems an implementation of a system is automatically constructed f… show more
PDF

Highlights - Most important sentences from the article

2018-08-28
1808.09430 | cs.LO

Reactive synthesis is an automatic way to translate a human intention expressed in some logic into a… show more
PDF

Highlights - Most important sentences from the article

2015-01-23
1501.05936 | cs.SY

This paper presents a novel approach to including non-instantaneous discrete control transitions in … show more
PDF

Highlights - Most important sentences from the article

2014-07-21
1407.5399 | cs.SE

Reactive synthesis deals with the automated construction of implementations of reactive systems from… show more
PDF

Highlights - Most important sentences from the article

2013-11-18
1311.4303 | cs.NI

Despite its great importance, modern network infrastructure is remarkable for the lack of rigor in i… show more
PDF

Highlights - Most important sentences from the article