4 citations · 14 across the 22 of their papers we have counts for
22 papers
Optimal LTLf Synthesis
Yujian Cao, Sven Schewe, Qiyi Tang +1
Strategy synthesis typically follows an all-or-nothing paradigm, returning unrealisable whenever a specification cannot be guaranteed in an uncertain environment. In this paper, we…
Fast Obligation Translation and Synthesis
Alexandre Duret-Lutz, Giuseppe De Giacomo, Marcin Jurdzinski +3
Syntactic obligations are a fragment of LTL formulas that translate to deterministic weak -automata (DWA). We show that syntactic obligations can be very efficiently converted t…
On-the-fly LTLf Synthesis under Partial Observability
Nadav Alon, Supratik Chakraborty, Alexandre Duret-Lutz +4
LTLf synthesis under partial observability requires reasoning about unobservable environment variables, which is typically handled by constructing a belief-state DFA via subset con…
The Complexity of Games with Randomised Control
Sarvin Bahmani, Rasmus Ibsen-Jensen, Soumyajit Paul +5
We study the complexity of solving two-player infinite duration games played on a fixed finite graph, where the control of a node is not predetermined but rather assigned randomly.…
A Compositional Framework for On-the-Fly LTLf Synthesis
Yongkang Li, Shengping Xiao, Shufang Zhu +2
Reactive synthesis from Linear Temporal Logic over finite traces (LTLf) can be reduced to a two-player game over a Deterministic Finite Automaton (DFA) of the LTLf specification. T…
Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis
Daniel Hausmann, Shufang Zhu, Gianmarco Parretti +3
Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLfp and PPLTLp, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings…
Engineering an LTLf Synthesis Tool
Alexandre Duret-Lutz, Shufang Zhu, Nir Piterman +2
The problem of LTLf reactive synthesis is to build a transducer, whose output is based on a history of inputs, such that, for every infinite sequence of inputs, the conjoint evolut…
LTLf Adaptive Synthesis for Multi-Tier Goals in Nondeterministic Domains
Giuseppe De Giacomo, Gianmarco Parretti, Shufang Zhu
We study a variant of LTLf synthesis that synthesizes adaptive strategies for achieving a multi-tier goal, consisting of multiple increasingly challenging LTLf objectives in nondet…
Learning to Coordinate without Communication under Incomplete Information
Shenghui Chen, Shufang Zhu, Giuseppe De Giacomo +1
Achieving seamless coordination in cooperative games is a crucial challenge in artificial intelligence, particularly when players operate under incomplete information. While commun…
On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts
Shengping Xiao, Yongkang Li, Shufang Zhu +4
We present an on-the-fly synthesis framework for Linear Temporal Logic over finite traces (LTLf) based on top-down deterministic automata construction. Existing approaches rely on…
The Trembling-Hand Problem for LTLf Planning
Pian Yu, Shufang Zhu, Giuseppe De Giacomo +2
Consider an agent acting to achieve its temporal goal, but with a "trembling hand". In this case, the agent may mistakenly instruct, with a certain (typically small) probability, a…
LTLf Best-Effort Synthesis in Nondeterministic Planning Domains
Giuseppe De Giacomo, Gianmarco Parretti, Shufang Zhu
We study best-effort strategies (aka plans) in fully observable nondeterministic domains (FOND) for goals expressed in Linear Temporal Logic on Finite Traces (LTLf). The notion of…
LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties
Benjamin Aminof, Giuseppe De Giacomo, Antonio Di Stasio +3
In this paper, we study LTLf synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks…
Symbolic LTLf Best-Effort Synthesis
Giuseppe De Giacomo, Gianmarco Parretti, Shufang Zhu
We consider an agent acting to fulfil tasks in a nondeterministic environment. When a strategy that fulfills the task regardless of how the environment acts does not exist, the age…
Act for Your Duties but Maintain Your Rights
Shufang Zhu, Giuseppe De Giacomo
Most of the synthesis literature has focused on studying how to synthesize a strategy to fulfill a task. This task is a duty for the agent. In this paper, we argue that intelligent…
Mimicking Behaviors in Separated Domains
Giuseppe De Giacomo, Dror Fried, Fabio Patrizi +1
Devising a strategy to make a system mimicking behaviors from another system is a problem that naturally arises in many areas of Computer Science. In this work, we interpret this p…
On the Power of Automata Minimization in Reactive Synthesis
Shufang Zhu, Lucas M. Tabajara, Geguang Pu +1
Temporal logic is often used to describe temporal properties in AI applications. The most popular language for doing so is Linear Temporal Logic (LTL). Recently, LTL on finite trac…
LTLf Synthesis with Fairness and Stability Assumptions
Shufang Zhu, Giuseppe De Giacomo, Geguang Pu +1
In synthesis, assumptions are constraints on the environment that rule out certain environment behaviors. A key observation here is that even if we consider systems with LTLf goals…
A Symbolic Approach to Safety LTL Synthesis
Shufang Zhu, Lucas M. Tabajara, Jianwen Li +2
Temporal synthesis is the automated design of a system that interacts with an environment, using the declarative specification of the system's behavior. A popular language for prov…
Symbolic LTLf Synthesis
Shufang Zhu, Lucas M. Tabajara, Jianwen Li +2
LTLf synthesis is the process of finding a strategy that satisfies a linear temporal specification over finite traces. An existing solution to this problem relies on a reduction to…
Safety Model Checking with Complementary Approximations
Jianwen Li, Shufang Zhu, Yueling Zhang +2
Formal verification techniques such as model checking, are becoming popular in hardware design. SAT-based model checking techniques such as IC3/PDR, have gained a significant succe…
SAT-based Explicit LTL Reasoning
Jianwen Li, Shufang Zhu, Geguang Pu +1
We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. As a proof-of-concept of th…