ML p(r)ior | Synthesizing a Lego Forklift Controller in GR(1): A Case Study

Synthesizing a Lego Forklift Controller in GR(1): A Case Study

2016-02-03
1602.01172 | cs.SE
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. GR(1) is a well-known fragment of linear temporal logic (LTL) where synthesis is possible using a polynomial symbolic algorithm. We conducted a case study to learn about the challenges that software engineers may face when using GR(1) synthesis for the development of a reactive robotic system. In the case study we developed two variants of a forklift controller, deployed on a Lego robot. The case study employs LTL specification patterns as an extension of the GR(1) specification language, an examination of two specification variants for execution scheduling, traceability from the synthesized controller to constraints in the specification, and generated counter strategies to support understanding reasons for unrealizability. We present the specifications we developed, our observations, and challenges faced during the case study.
PDF

Highlights - Most important sentences from the article

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

Related Articles

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-10-12

This paper introduces assume/guarantee contracts on continuous-time control systems, hereby extendin… show more
PDF

Highlights - Most important sentences from the article

2019-02-27

We consider the problem of extracting safe environments and controllers for reach-avoid objectives f… show more
PDF

Highlights - Most important sentences from the article

2019-01-09

In cyber-physical systems like automotive systems, there are components like sensors, actuators, and… 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

2019-03-29

Debugging Cyber-Physical System (CPS) models can be extremely complex. Indeed, only the detection of… 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

2019-03-04

With the primary objective of human-robot interaction being to support humans' goals, there exists a… 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

2019-06-05

The paper presents a software architecture to optimize the process of prototyping and deploying robo… show more
PDF

Highlights - Most important sentences from the article

2017-05-23

LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification o… show more
PDF

Highlights - Most important sentences from the article

2012-07-04

We demonstrate the modelling of opportunistic networks using the process algebra stochastic HYPE. Ne… 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

2016-03-08
1603.02650 | cs.SY

The fundamental idea of this work is to synthesize reactive controllers such that closed-loop execut… show more
PDF

Highlights - Most important sentences from the article