Formalizing synthesis in TLA+
- Creators
-
Filippidis, Ioannis
-
Murray, Richard M.
Abstract
This report proposes a TLA+ definition for the problem of constructing a strategy that implements a temporal property. It is based on a note by Lamport [1] that outlines a formalization of realizability in TLA. The modified definition proposed here is expressed axiomatically in TLA+. Specifying what function is acceptable as a strategy requires care, so that a function with empty domain be avoided, while ensuring that the strategy will not need to have a domain too large to be a set. We prove that initial conditions should appear in assumptions only, unless an initial predicate is added to the definition of a realization. We show that a specification should include an assumption about a set of initial values to ensure that realizability does not become unprovable. We discuss what form of open-system properties expressed with the "while- plus" operator -+-> are realizable. We formalize the notions of interleaving and disjoint-state behaviors, based on definitions given by Lamport and Abadi, and consider the notion of interleaving for an open-system property. We give examples of expressing different forms of games in TLA+ using the proposed definition, including games with partial information.
Additional Information
The authors would like to thank Scott Livingston for providing feedback on drafts of this manuscript, and Necmiye Ozay for interesting discussions related to synthesis. This work was supported in part by the TerraSwarm Research Center, one of six centers supported by the STARnet phase of the Focus Center Research Program (FCRP), a Semiconductor Research Corporation program sponsored by MARCO and DARPA.Attached Files
Draft - 20161223.pdf
Files
Name | Size | Download all |
---|---|---|
md5:526dba923c028de9f25f534ad618397a
|
268.5 kB | Preview Download |
Additional details
- Eprint ID
- 73165
- Resolver ID
- CaltechCDSTR:2016.004
- TerraSwarm Research Center
- Semiconductor Research Corporation
- Microelectronics Advanced Research Corporation (MARCO)
- Defense Advanced Research Projects Agency (DARPA)
- STARnet
- Created
-
2016-12-23Created from EPrint's datestamp field
- Updated
-
2019-10-03Created from EPrint's last_modified field
- Caltech groups
- Control and Dynamical Systems Technical Reports