Finite-Trace and Generalized-Reactivity Specifications in Temporal Synthesis

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2021/255 ◽

2021 ◽

Author(s):

Giuseppe De Giacomo ◽

Antonio Di Stasio ◽

Lucas M. Tabajara ◽

Moshe Vardi ◽

Shufang Zhu

Keyword(s):

Temporal Logic ◽

Linear Temporal Logic ◽

Specification Language ◽

Ai Planning ◽

Success Stories ◽

Ltl Synthesis ◽

Finite Trace

Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTLf (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTLf agent goal and a GR(1) assumption. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis.

Download Full-text

Extending Linear Temporal Logic with Clocks to Object-Z

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.513-517.927 ◽

2014 ◽

Vol 513-517 ◽

pp. 927-930

Author(s):

Zhi Cheng Wen ◽

Zhi Gang Chen

Keyword(s):

Real Time ◽

Temporal Logic ◽

Formal Specification ◽

Large Scale ◽

Linear Temporal Logic ◽

Specification Language ◽

Continuous Variables ◽

Real Time System ◽

Software Specification ◽

Formal Specification Language

Object-Z, an extension to formal specification language Z, is good for describing large scale Object-Oriented software specification. While Object-Z has found application in a number of areas, its utility is limited by its inability to specify continuous variables and real-time constraints. Linear temporal logic can describe real-time system, but it can not deal with time variables well and also can not describe formal specification modularly. This paper extends linear temporal logic with clocks (LTLC) and presents an approach to adding linear temporal logic with clocks to Object-Z. Extended Object-Z with LTLC, a modular formal specification language, is a minimum extension of the syntax and semantics of Object-Z. The main advantage of this extension lies in that it is convenient to describe and verify the complex real-time software specification.

Download Full-text

Assume-Guarantee Synthesis for Prompt Linear Temporal Logic

Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2020/17 ◽

2020 ◽

Author(s):

Nathanaël Fijalkow ◽

Bastien Maubert ◽

Aniello Murano ◽

Moshe Vardi

Keyword(s):

Temporal Logic ◽

Waiting Times ◽

Linear Temporal Logic ◽

Ltl Synthesis

Prompt-LTL extends Linear Temporal Logic with a bounded version of the ``eventually'' operator to express temporal requirements such as bounding waiting times. We study assume-guarantee synthesis for prompt-LTL: the goal is to construct a system such that for all environments satisfying a first prompt-LTL formula (the assumption) the system composed with this environment satisfies a second prompt-LTL formula (the guarantee). This problem has been open for a decade. We construct an algorithm for solving it and show that, like classical LTL synthesis, it is 2-EXPTIME-complete.

Download Full-text