Exploring Finite-Word Automata for Reactive Synthesis

Formal verification can provide confidence in the correctness of a system by checking that its implementation satisfies a formal specification of its desired behavior. Yet, a system might have to be implemented and reimplemented many times before passing verification. Program synthesis, on the other hand, presents an alternative workflow where the implementation is directly and algorithmically generated from the formal specification. One widely-studied example is reactive synthesis, which aims to synthesize a reactive system from a specification in some form of temporal logic. So far, reactive synthesis has largely resisted practical implementation, not only because of the problem's 2EXPTIME worst-case complexity, but also because algorithms often rely on manipulation of automata over infinite words, for which there are no known efficient algorithms. The goal of this thesis is to take steps towards bringing reactive synthesis to the realm of practical application by exploring the potential of synthesis algorithms using automata over finite words. Not only are finite-word automata sufficient for many use cases of reactive synthesis - for example in robotics, where systems are built to perform finite tasks - but they support algorithms that are far more efficient and amenable to implementation in practice than automata over infinite words. The work presented in this thesis demonstrates how specialized synthesis algorithms making use of automata over finite words perform significantly better in practice than general algorithms based on infinite-word automata, despite having the same theoretical complexity. It also explores how to improve the construction of such automata in a way that benefits synthesis algorithms. Finally, it shows how the algorithmic simplicity of finite-word automata allows the implementation for the first time of useful extensions of reactive synthesis that in the past have been limited purely to the realm of theory, such as synthesis under partial observability, allowing us to identify significant differences between the theoretical analysis and practical performance of the algorithms.

Name thesis:degree_name

Doctor of Philosophy

Level thesis:degree_level

Doctoral

Discipline thesis:degree_discipline

Engineering

Grantor

Rice University

Year dc:date.issued

2021

Author dc:creator

• Martinelli Tabajara, Lucas

Advisor dc:contributor.advisor

• Vardi, Moshe Y.

• Formal methods
• Reactive synthesis
• Finite automata

Statement dc:rights

• Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder.

Language dc:language.iso

eng

Handle dc:identifier.uri

https://hdl.handle.net/1911/111221

OAI identifier oai:identifier

oai:repository.rice.edu:1911/111221