Title: Theory / Unimportant / CS / Fundamental / Model Checking / toSort / On the synthesis of a Reactive Module
Tags: examplesSwitchExample1

Smaller0: \(\forall x\exists y\phi(x,y)\)
Greater0: \(\exists f\forall x\phi(x,f(y))\)
Page: 1
Chapter: On the synthesis of a Recative Module
Variables: \(x,y\) variables,
\(\phi(x,y)\) a formula
Smaller to greater: is equivalent to
Name: Skolem paradigm
Name2: AE paradigm

Name: Synthesis by theorem proving
Definition: Given a formula \(\phi(x,y)\), search for a proof of \(\forall x\exists y\phi(x,y)\) using a constructive proof system. It gives an algo from \(x\) to some \(y\)
Page: 1
Chapter: On the synthesis of a Recative Module
Example: \(|x-y^2|<\epsilon\) states that \(y\) is a good approximation of \(x\)'s square root

Name: A synchronous program from \(D\) to \(D\)
Definition: A function \(D^+\to D\)
Page: 4
Chapter: On the synthesis of a Recative Module
Section: 3
Variables: \(D\) an alphabet
Denoted by: \(P\) or \(f_P\)

Name: The behavior of \(P\)
Definition: An infinite sequence \((\langle a_i,b_i\rangle)\) such that \(b_i=f_P(a_0\dots a_i)\)
Page: 5
Chapter: On the synthesis of a Recative Module
Section: 3
Variables: \(D\) an alphabet,
\(P\) a synchronous program from \(D\) to \(D\)
Denoted by: \(\sigma\)

Name: \(P\) satisfies \(\phi\)
Definition: Every behavior of \(P\) satisfies \(\phi(x,y)\)
Page: 5
Chapter: On the synthesis of a Recative Module
Section: 3
Variables: \(D\) an alphabet,
\(P\) a synchronous program from \(D\) to \(D\)
\(\phi(x,y)\) an LTL specification
Notation: \(P\models\phi(x,y)\)

Name: An implementable specification
Definition: A specification such that there exists a program which satisfies this specification.
Page: 5
Chapter: On the synthesis of a Recative Module
Section: 3

Name: An implementation of \(\phi\)
Definition: A program which satisfies \(\phi\)
Page: 5
Chapter: On the synthesis of a Recative Module
Section: 3
Variables: \(\phi(x,y)\) a specification

Smaller0: \(\phi(x,y)\) is implementable
Greater0: \(\phi(x,y)\) is satisfiable
Page: 5
Chapter: On the synthesis of a Recative Module
Section: 3
Variables: \(\phi(x,y)\) a specification
Greater1: \(\forall x\exists y\phi(x,y)\) is valid
Counterexample: \(\circ x\)
\((y\iff\diamond x)\)

Definition: \(\neg E\neg p\)
Page: 182
Chapter: On the synthesis of reactive module
Variables: \(p\) a path formula
Notation: \(Ap\)