A Caltech Library Service

Formalizing synthesis in TLA+

Filippidis, Ioannis and Murray, Richard M. (2016) Formalizing synthesis in TLA+. , Pasadena, CA. (Unpublished)

[img] PDF - Draft Version
Creative Commons Attribution Non-commercial No Derivatives.


Use this Persistent URL to link to this item:


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.

Item Type:Report or Paper (Technical Report)
Filippidis, Ioannis0000-0003-4704-3334
Murray, Richard M.0000-0002-5785-7481
Contact Email
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.
Group:Control and Dynamical Systems Technical Reports
Funding AgencyGrant Number
TerraSwarm Research CenterUNSPECIFIED
Semiconductor Research CorporationUNSPECIFIED
Microelectronics Advanced Research Corporation (MARCO)UNSPECIFIED
Defense Advanced Research Projects Agency (DARPA)UNSPECIFIED
Record Number:CaltechCDSTR:2016.004
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:73165
Deposited By: Ioannis Filippidis
Deposited On:23 Dec 2016 15:53
Last Modified:03 Oct 2019 16:25

Repository Staff Only: item control page