-
Article
Open AccessGR(1)*: GR(1) specifications extended with existential guarantees
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables effi...
-
Chapter and Conference Paper
Efficient Algorithms for Omega-Regular Energy Games
\(\omega \) ω -regular energy games are two-player ...
-
Chapter and Conference Paper
Adapting Behaviors via Reactive Synthesis
In the Adapter Design Pattern, a programmer implements a Target interface by constructing an Adapter that accesses an existing Adaptee code. In this work, we present a reactive synthesis interpretation to the ada...
-
Chapter and Conference Paper
GR(1)*: GR(1) Specifications Extended with Existential Guarantees
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables effi...
-
Chapter and Conference Paper
The F-Snapshot Problem
Aguilera, Gafni and Lamport introduced the signaling problem in [3]. In this problem, two processes numbered 0 and 1 can call two procedures: update and Fscan. A parameter of the problem is a two-variable functio...
-
Chapter and Conference Paper
On the Mailbox Problem
The Mailbox Problem was described and solved by Aguilera, Gafni, and Lamport in [2] with a mailbox algorithm that uses two flag registers that carry 14 values each. An interesting question that they ask is whe...
-
Chapter and Conference Paper
On the Signaling Problem
Aguilera et al. introduced and solved the mailbox problem in [4], and used their mailbox algorithm to provide an efficient solution to the N-buffer problem. In the same paper, they also pointed out that both the ...
