Vacuity in synthesis

Roderick Bloem; Hana Chockler; Masoud Ebrahimi; Ofer Strichman

doi:10.1007/s10703-021-00381-5

Vacuity in synthesis

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman^*

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

2 Citations (Scopus)

Abstract

In reactive synthesis, one begins with a temporal specification φ, and automatically synthesizes a system M such that M⊧ φ. As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies φnon-vacuously, then M is likely to be closer to the user’s intent, because it satisfies φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.

Original language	English
Pages (from-to)	473-495
Number of pages	23
Journal	FORMAL METHODS IN SYSTEM DESIGN
Volume	57
Issue number	3
DOIs	https://doi.org/10.1007/s10703-021-00381-5
Publication status	Published - Sept 2021

Keywords

Bounded synthesis
Reactive synthesis
Vacuity

Access to Document

10.1007/s10703-021-00381-5

Cite this

@article{3a89692b9a7e4756a5f4f4c5332eb074,

title = "Vacuity in synthesis",

abstract = "In reactive synthesis, one begins with a temporal specification φ, and automatically synthesizes a system M such that M⊧ φ. As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies φnon-vacuously, then M is likely to be closer to the user{\textquoteright}s intent, because it satisfies φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer{\textquoteright}s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.",

keywords = "Bounded synthesis, Reactive synthesis, Vacuity",

author = "Roderick Bloem and Hana Chockler and Masoud Ebrahimi and Ofer Strichman",

note = "Funding Information: This work was supported by the Austrian Research Promotion Agency (FFG) through project TRUSTED (867558), Graz University of Technology{\textquoteright}s LEAD project “Dependable Internet of Things in Adverse Environments”. Publisher Copyright: {\textcopyright} 2021, The Author(s). Copyright: Copyright 2021 Elsevier B.V., All rights reserved.",

year = "2021",

month = sep,

doi = "10.1007/s10703-021-00381-5",

language = "English",

volume = "57",

pages = "473--495",

journal = "FORMAL METHODS IN SYSTEM DESIGN",

issn = "0925-9856",

publisher = "Springer Netherlands",

number = "3",

}

TY - JOUR

T1 - Vacuity in synthesis

AU - Bloem, Roderick

AU - Chockler, Hana

AU - Ebrahimi, Masoud

AU - Strichman, Ofer

N1 - Funding Information: This work was supported by the Austrian Research Promotion Agency (FFG) through project TRUSTED (867558), Graz University of Technology’s LEAD project “Dependable Internet of Things in Adverse Environments”. Publisher Copyright: © 2021, The Author(s). Copyright: Copyright 2021 Elsevier B.V., All rights reserved.

PY - 2021/9

Y1 - 2021/9

N2 - In reactive synthesis, one begins with a temporal specification φ, and automatically synthesizes a system M such that M⊧ φ. As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies φnon-vacuously, then M is likely to be closer to the user’s intent, because it satisfies φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.

AB - In reactive synthesis, one begins with a temporal specification φ, and automatically synthesizes a system M such that M⊧ φ. As many systems can satisfy a given specification, it is natural to seek ways to force the synthesis tool to synthesize systems that are of a higher quality, in some well-defined sense. In this article we focus on a well-known measure of the way in which a system satisfies its specification, namely vacuity. Our conjecture is that if the synthesized system M satisfies φnon-vacuously, then M is likely to be closer to the user’s intent, because it satisfies φ in a more “meaningful” way. Narrowing the gap between the formal specification and the designer’s intent in this way, automatically, is the topic of this article. Specifically, we propose a bounded synthesis method for achieving this goal. The notion of vacuity as defined in the context of model checking, however, is not necessarily refined enough for the purpose of synthesis. Hence, even when the synthesized system is technically non-vacuous, there are yet more interesting (equivalently, less vacuous) systems, and we would like to be able to synthesize them. To that end, we cope with the problem of synthesizing a system that is as non-vacuous as possible, given that the set of interesting behaviours with respect to a given specification induce a partial order on transition systems. On the theoretical side we show examples of specifications for which there is a single maximal element in the partial order (i.e., the most interesting system), a set of equivalent maximal elements, or a number of incomparable maximal elements. We also show examples of specifications that induce infinite chains of increasingly interesting systems. These results have implications on how non-vacuous the synthesized system can be. We implemented the new procedure in our synthesis tool PARTY. For this purpose we added to it the capability to synthesize a system based on a property which is a conjunction of universal and existential LTL formulas.

KW - Bounded synthesis

KW - Reactive synthesis

KW - Vacuity

UR - http://www.scopus.com/inward/record.url?scp=85115109445&partnerID=8YFLogxK

U2 - 10.1007/s10703-021-00381-5

DO - 10.1007/s10703-021-00381-5

M3 - Article

AN - SCOPUS:85115109445

SN - 0925-9856

VL - 57

SP - 473

EP - 495

JO - FORMAL METHODS IN SYSTEM DESIGN

JF - FORMAL METHODS IN SYSTEM DESIGN

IS - 3

ER -

Vacuity in synthesis

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this