Title: Theory / Unimportant / CS / Fundamental / Model Checking / toSort
Tags: hasSeenConjDef récupéré closed fromMath mathToSee toAutomata toBinaryFunction toQuestion

Name: The class of deterministic timed automata
Page: 5
Section: 2
Under: synchronized product

Definition: The set of formulas to be covered but still not processed.
Page: 252
Section: 3.1
Variables: \(\psi\) an LTL formula
Notation: ToCover

Definition: The element of the cover currently being computed.
Page: 252
Section: 3.1
Variables: \(\psi\) an LTL formula
Notation: Current

Definition: The formulas already processed and covered by Current.
Page: 252
Section: 3.1
Variables: \(\psi\) an LTL formula
Notation: Covered

Definition: The cover so far computed.
Page: 252
Section: 3.1
Variables: \(\psi\) an LTL formula
Notation: Cover

Name: A fair discrete system
Definition: \(V=\{u_1,\dots, u_n\}\) a finite set of typed state variables, over possibly infinite domain.
Page: 5
Section: 2
Index: 1
Kind: Lem
Definition2: \(\Theta\): the initial condition. An assertion characterizing all the initial states.
Conjdef: A tuple
Definition3: \(\rho\): A transition relation. An assertion over two copies of the state variables of \(V\), without prime for initial state and primed for the successor state
Abbreviation: FDS
Definition4: \(\mathcal J\): A set of assertions expressing the justice (weak fairness) requirements.
Denoted by: \(\mathcal D\)
Definition5: \(\mathcal C=\{\langle p_1,q_1\rangle,\dots,\langle p_n,q_n\rangle\}\) A set of assertions expressing the compassion (strong fairness) requirements

Name: A state
Definition: A type-consistent interpretation of \(V\)
Page: 5
Section: 2
Variables: \(\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
Denoted by: \(s\)

Definition: The value of the variable \(u\) in state \(s\)
Page: 5
Section: 2
Variables: \(\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
\(u\in V\),
\(s\) a state
Notation: \(s[u]\)

Definition: The set of states
Page: 5
Section: 2
Variables: \(\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
Notation: \(\Sigma\)

Name: A \(\phi\)-position of \(\sigma\)
Definition: An integer \(j\) such that \(s_j\) is a \(\phi\)-state
Page: 5
Section: 2
Variables: \(\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
\(\sigma:s_0\dots \) a sequence of state,
\(\phi\) an assertion

Name: A run of \(\mathcal D\)
Definition: Initiality: \(s_0\) is initial, i.e. \(s_0\models\Theta\)
Page: 6
Section: 2
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
Definition2: Consecution: For each \(j+1\in[1,|\sigma|)\), \(s_{j+1}\) is a \(\mathcal D\) successor of \(s_j\)
Conjdef: A sequence of states \(\sigma:s_0\dots\) such that
Definition3: Either \(\sigma\) is infinite, or \(s_{|\sigma|-1}\) has no \(\mathcal D\)-successor.
Name2: A path in \(\mathcal D\)

Name: A computation of \(\mathcal D\)
Definition: \(\sigma\) is infinite
Page: 6
Section: 2
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
Definition2: Justice: for each \(J\in\mathcal J\), \(\sigma\) contains infinitely many \(J\)-positions
Conjdef: A run \(\sigma=s_0\dots\) of \(\mathcal D\)
Definition3: Compassion: for each \(\langle p,q\rangle\in\mathcal C\), if \(\sigma\) contains infinitely many \(p\)-positions, it must contains infinitely many \(q\)-positions
Name2: A fair path in \(\mathcal D\)
Extra: initial ?

Name: The set of runs of \(\mathcal D\)
Page: 6
Section: 2
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
Notation: \(runs(\mathcal D)\)

Name: The set of computations of \(\mathcal D\)
Page: 6
Section: 2
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
Abbreviation: \(Comp(\mathcal D)\)

Name: A reachable state
Definition: A state participing in some run of \(\mathcal D\)
Page: 6
Section: 2
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,

Name: A feasible state
Definition: A state participing in some computation of \(\mathcal D\)
Page: 6
Section: 2
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS

Name: A deadlock-free FDS
Definition: An FDS such that every reachable states has a \(\mathcal D\)-successor.
Page: 6
Section: 2

Smaller0: \(\mathcal D\) is deadlock-free
Greater0: \(\sigma\) is infinite
Page: 6
Section: 2
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
\(\sigma=s_0\dots\) a run
Smallest: \(\mathcal D\) is viable

Name: A feasible FDS
Definition: A feasible with at least one computation
Page: 6
Section: 2

Name: A viable FDS
Definition: A FDS whose every reachable state is feasible.
Page: 6
Section: 2

Page: 6
Section: 2.1
Notation: \(\mathcal D_1|||\mathcal D_2\)
Variables: \(\mathcal D_i=\langle V_i,\Theta_i,\rho_i,\mathcal J_i,\mathcal C_i\rangle\) an FDS,
Name: The synchronous parallel composition of \(\mathcal D_1\) and \(\mathcal D_2\)
Definition: states variables are \(V_1\cup V_2\)
Definition2: Initial condition \(\Theta_1\land \Theta_2\)
ConjDef: The FDS
Definition3: Transition relation \(\rho_1\land\rho_2\)
Definition4: Fairness and compassion are the unions of the elements of each FDS

Definition: \(\bigwedge_{v\in U}v=v'\)
Page: 6
Section: 2.1
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
\(U\subseteq V\)
Notation: \(pres(U)\)
Conjdef: The FDS

Definition: states variables are \(V_1\cup V_2\)
Page: 6
Section: 2.1
Variables: \(\mathcal D_i=\langle V_i,\Theta_i,\rho_i,\mathcal J_i,\mathcal C_i\rangle\) an FDS,
Notation: \(\mathcal D_1\parallel\mathcal D_2\)
Definition2: Initial condition \(\Theta_1\land \Theta_2\)
Conjdef: The FDS
Definition3: Transition relation \(\bigvee_i\rho_i\land \bigwedge_{j\in V_{3-i}\setminus V_i}\)
Definition4: Fairness and compassion are the unions of the elements of each FDS

Name: An interleaved execution of \(\mathcal D_1\) and \(\mathcal D_2\)
Definition: An execution of \(\mathcal D_1\parallel\mathcal D_2\)
Page: 6
Section: 2.1
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,

Name: A just discrete system
Definition: An FDS without compassion requirements
Page: 7
Section: 2.2
Abbreviation: A JDS

Name: An equivalent JDS
Definition: The variables are: the variables of \(V\), and a Boolean \(n\_p_i\) for each \((p_i,q_i)\in\mathcal C\}\) and \(x_c\)
Page: 7
Section: 2.2
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
\(\sigma=s_0\dots\) a run
Definition2: Initial state is the conjunction of \(\Theta\), \(x_c=0\) and \(n\_p_i=0\) for each \((p_i,q_i)\in \mathcal C\)
Conjdef: A JDS
Definition3: Transition relation is the conjunction of \(\rho\),
\((n\_p_i\to n\_p'_i)\) for each \((p_i,q_i)\in \mathcal C\) and \(x'_c=x_c\lor \bigvee_{(p_i,q_i)\in\mathcal C}(p_i\land n\_p_i)\)
Intuition: \(n\_p_i\) turns true when \(p_i\) holds and no \(q_i\) occurs later
\(x_c\) becomes true when some \(n\_p_i\) becomes true
Definition4: The justices requirements are: the ones of \(\mathcal J\), \(\neg x_c\), and \(n\_p_i\lor q_i\) for each \((p_i,q_i)\in\mathcal C\)

Name: The future fragment of CTL*
Definition: The restriction of CTL without the past operators
Page: 8
Section: 3

Name: An existential fair path quantifiers
Page: 8
Section: 3
Notation: \(E_f\)

Name: A universal fair path quantifiers
Page: 8
Section: 3
Notation: \(A_f\)

Name: A basic state formula
Definition: A formula \(\mathcal Q\psi\) with \(\mathcal Q\in\{E,A,E_f,A_f\}\) and \(\psi\) a path formula containing no other path quantifier
Page: 9
Section: 3.1

Name: A basic assertionnal formula
Definition: A formula \(\mathcal Qp\) with \(\mathcal Q\in\{E,A,E_f,A_f\}\) and \(p\) an assertion
Page: 9
Section: 3.1

Name: A basic path formula
Definition: A path formula whose principal operator is temporal, which contains no other temporal operators or path quantifiers
Page: 9
Section: 3.1

Name: The vocabulary of \(p\)
Definition: The set of variables occurring in \(p\)
Page: 9
Section: 3.1
Variables: \(p\) a formula

Definition: if \(p\) is a state formula, \((\mathcal D,\pi[j])\models p\)
Page: 9
Section: 3.1
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
\(\pi\) a path
\(j\in[0..|\pi|)\)
Notation: \((\mathcal D,\pi,j)\models p\)
Definition2: if \(p=q\), \(j=0\) or \((\mathcal D,\pi,j-1)\models p\)
Conjdef: Either
Definition3: The remaining as usual

Definition: if \(p\) is an assertion, \(s\models p\)
Page: 9
Section: 3.1
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
\(s\) a state
Notation: \((\mathcal D,s)\models p\)
Definition2: Conjunction, disjunction as usual
Definition3: for \(p= Eq\), \((\mathcal D,\pi,j)\models q\) for some path \(\pi\in runs(\mathcal D)\) and position \(j\in[0..|\pi|)\) satisfying \(\pi[j]=s\). Similarly for \(p=Aq\)
Definition4: for \(p=E_fq\) and \(p=A_fq\), the quantification is restrected to fair path

Name: A formula which is \(\mathcal D\)-valid
Definition: A CTL* formula \(p\) such that \((\mathcal D,s)\models p\) for every initial state \(s\) in \(\mathcal D\)
Page: 10
Section: 3.1
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
\(p\) a CTL* formula
Notation: \(\mathcal D\models p\)
Name2: A formula which holds on \(\mathcal D\)

Name: A satisfiable CTL* formula
Definition: A formula which holds on some model
Page: 10
Section: 3.1

Name: A valid CTL* formula
Definition: A formula which holds on all model
Page: 10
Section: 3.1

Name: A \(p\)-state
Definition: A state which holds at \(p\)
Page: 10
Section: 3.1
Variables: \(\mathcal D=\langle V,\Theta,\rho,\mathcal{J,C}\rangle\) an FDS,
\(p\) a CTL* formula