:: Model Checking, Part {I}
:: by Kazuhisa Ishida
::
:: Received November 14, 2006
:: Copyright (c) 2006-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, ARYTM_3, XXREAL_0, SUBSET_1, CARD_1, FUNCT_1,
RELAT_1, XBOOLEAN, TARSKI, XBOOLE_0, FINSEQ_1, ZF_LANG, ORDINAL4,
PARTFUN1, ZFMISC_1, BINOP_1, FUNCOP_1, FUNCT_2, FUNCT_7, ORDERS_1,
MARGREL1, ZF_MODEL, ARYTM_1, FUNCT_3, COHSP_1, ABIAN, KNASTER, MODELC_1,
STRUCT_0, ORDERS_2, FUNCT_5, ROBBINS1, LATTICES;
notations RELSET_1, RELAT_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_7, BINOP_1,
FINSEQ_1, PARTFUN1, KNASTER, XXREAL_0, ABIAN, ORDERS_1, FUNCOP_1,
MARGREL1, FUNCT_5, STRUCT_0, ORDERS_2, LATTICES, ROBBINS1;
constructors BINOP_1, FUNCT_3, REAL_1, NAT_1, MARGREL1, ABIAN, KNASTER,
RELSET_1, FUNCT_5, ROBBINS1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, XXREAL_0,
XREAL_0, NAT_1, INT_1, XBOOLEAN, MARGREL1, KNASTER, CARD_1, RELSET_1,
STRUCT_0;
requirements REAL, NUMERALS, ARITHM, SUBSET, BOOLE;
begin
definition
let x be object, S be set; :: !!! zastapic przez In(.,.)
let a be Element of S;
func k_id(x,S,a) -> Element of S equals
:: MODELC_1:def 1
x if x in S otherwise a;
end;
definition
let x be object;
func k_nat(x) -> Element of NAT equals
:: MODELC_1:def 2
x if x in NAT otherwise 0;
end;
definition
let f be Function;
let x,a be set;
func UnivF(x,f,a) -> set equals
:: MODELC_1:def 3
f.x if x in dom f otherwise a;
end;
definition
let a be set;
func Castboolean(a) -> boolean object equals
:: MODELC_1:def 4
a if a is boolean
otherwise FALSE;
end;
definition
let X be set, a be object; :: zastapic przez In(.,.) !!!
func CastBool(a,X) -> Subset of X equals
:: MODELC_1:def 5
a if a in bool X otherwise {};
end;
reserve k,n for Element of NAT,
a,Y for set,
D,D1,D2 for non empty set,
p,q for FinSequence of NAT;
:: The operations to make CTL-formulae
definition
let n;
func atom.n -> FinSequence of NAT equals
:: MODELC_1:def 6
<* (5 + n) *>;
end;
definition
let p;
func 'not' p -> FinSequence of NAT equals
:: MODELC_1:def 7
<*0*>^p;
let q;
func p '&' q -> FinSequence of NAT equals
:: MODELC_1:def 8
<*1*>^p^q;
end;
definition
let p;
func EX p -> FinSequence of NAT equals
:: MODELC_1:def 9
<*2*>^p;
func EG p -> FinSequence of NAT equals
:: MODELC_1:def 10
<*3*>^p;
let q;
func p EU q -> FinSequence of NAT equals
:: MODELC_1:def 11
<*4*>^p^q;
end;
:: The set of all well formed formulae of CTL-language
definition
func CTL_WFF -> non empty set means
:: MODELC_1:def 12
(for a st a in it holds a is
FinSequence of NAT ) & (for n holds atom.n in it ) & (for p st p in it holds
'not' p in it ) & (for p,q st p in it & q in it holds p '&' q in it ) & (for p
st p in it holds EX p in it ) & (for p st p in it holds EG p in it ) & (for p,q
st p in it & q in it holds p EU q in it ) & for D st (for a st a in D holds a
is FinSequence of NAT ) & (for n holds atom.n in D ) & (for p st p in D holds
'not' p in D ) & (for p,q st p in D & q in D holds p '&' q in D ) & (for p st p
in D holds EX p in D ) & (for p st p in D holds EG p in D ) & (for p,q st p in
D & q in D holds p EU q in D ) holds it c= D;
end;
definition
let IT be FinSequence of NAT;
attr IT is CTL-formula-like means
:: MODELC_1:def 13
IT is Element of CTL_WFF;
end;
registration
cluster CTL-formula-like for FinSequence of NAT;
end;
definition
mode CTL-formula is CTL-formula-like FinSequence of NAT;
end;
theorem :: MODELC_1:1
a is CTL-formula iff a in CTL_WFF;
reserve F,F1,G,G1,H,H1,H2 for CTL-formula;
registration
let n;
cluster atom.n -> CTL-formula-like;
end;
registration
let H;
cluster 'not' H -> CTL-formula-like;
cluster EX H -> CTL-formula-like;
cluster EG H -> CTL-formula-like;
let G;
cluster H '&' G -> CTL-formula-like;
cluster H EU G -> CTL-formula-like;
end;
definition
let H;
attr H is atomic means
:: MODELC_1:def 14
ex n st H = atom.n;
attr H is negative means
:: MODELC_1:def 15
ex H1 st H = 'not' H1;
attr H is conjunctive means
:: MODELC_1:def 16
ex F,G st H = F '&' G;
attr H is ExistNext means
:: MODELC_1:def 17
ex H1 st H = EX H1;
attr H is ExistGlobal means
:: MODELC_1:def 18
ex H1 st H = EG H1;
attr H is ExistUntill means
:: MODELC_1:def 19
ex F,G st H = F EU G;
end;
definition
let F,G;
func F 'or' G -> CTL-formula equals
:: MODELC_1:def 20
'not'('not' F '&' 'not' G);
end;
theorem :: MODELC_1:2
H is atomic or H is negative or H is conjunctive or H is
ExistNext or H is ExistGlobal or H is ExistUntill;
reserve sq,sq9 for FinSequence;
definition
let H;
assume
H is negative or H is ExistNext or H is ExistGlobal;
func the_argument_of H -> CTL-formula means
:: MODELC_1:def 21
'not' it = H if H is
negative, EX it = H if H is ExistNext otherwise EG it = H;
end;
definition
let H;
assume
H is conjunctive or H is ExistUntill;
func the_left_argument_of H -> CTL-formula means
:: MODELC_1:def 22
ex H1 st it '&' H1 = H if H is conjunctive otherwise ex H1 st it EU H1 = H;
func the_right_argument_of H -> CTL-formula means
:: MODELC_1:def 23
ex H1 st H1 '&' it = H if H is conjunctive otherwise ex H1 st H1 EU it = H;
end;
definition
let x be object;
func CastCTLformula(x) -> CTL-formula equals
:: MODELC_1:def 24
x if x in CTL_WFF
otherwise atom.0;
end;
::***************************************************
::**
::** definition of Kripke structure & CTL model structure.
::**
::****************************************************
definition
let Prop be set;
struct(RelStr) KripkeStr over Prop (# carrier -> set,
Starts -> Subset of the carrier,
InternalRel -> Relation of the carrier, the carrier,
Label -> Function of the carrier, bool Prop #);
end;
definition
struct(ComplULattStr) CTLModelStr (# carrier -> set, BasicAssign ->
Subset of the carrier, L_meet -> BinOp of the carrier, Compl -> UnOp
of the carrier, EneXt -> UnOp of the carrier, EGlobal -> UnOp of the
carrier, EUntill -> BinOp of the carrier #);
end;
definition
let V be CTLModelStr;
mode Assign of V is Element of the carrier of V;
end;
:: Preparation to define semantics for CTL-language
:: definition of evaluate function of CTL
definition
func atomic_WFF -> Subset of CTL_WFF equals
:: MODELC_1:def 25
{x where x is CTL-formula:x is atomic};
end;
definition
let V be CTLModelStr;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let f be Function of CTL_WFF,the carrier of V;
pred f is-Evaluation-for Kai means
:: MODELC_1:def 26
for H being CTL-formula holds (H is atomic implies f.H = Kai.H) &
(H is negative implies f.H = (the Compl of V).(f
.(the_argument_of H))) &
(H is conjunctive implies f.H = (the L_meet of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))) & (H is ExistNext
implies f.H = (the EneXt of V).(f.(the_argument_of H))) & (H is ExistGlobal
implies f.H = (the EGlobal of V).(f.(the_argument_of H))) & (H is ExistUntill
implies f.H = (the EUntill of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)));
end;
definition
let V be CTLModelStr;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let f be Function of CTL_WFF,the carrier of V;
let n be Nat;
pred f is-PreEvaluation-for n,Kai means
:: MODELC_1:def 27
for H being CTL-formula st
len(H) <= n holds (H is atomic implies f.H = Kai.H) & (H is negative implies f.
H = (the Compl of V).(f.(the_argument_of H))) &
(H is conjunctive implies f.H = (
the L_meet of V).(f.(the_left_argument_of H), f.(the_right_argument_of H))) &
(H
is ExistNext implies f.H = (the EneXt of V).(f.(the_argument_of H))) & (H is
ExistGlobal implies f.H = (the EGlobal of V).(f.(the_argument_of H))) & (H is
ExistUntill implies f.H = (the EUntill of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)));
end;
definition
let V be CTLModelStr;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let f,h be Function of CTL_WFF,the carrier of V;
let n be Nat;
let H be CTL-formula;
func GraftEval(V,Kai,f,h,n,H) -> set equals
:: MODELC_1:def 28
f.H if len(H) > n+1, Kai
.H if len(H)=n+1 & H is atomic, (the Compl of V).(h.(the_argument_of H))
if len(H
)=n+1 & H is negative, (the L_meet of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) if len(H)=n+1 & H is conjunctive, (the EneXt of V).(h
.(the_argument_of H)) if len(H)=n+1 & H is ExistNext , (the EGlobal of V).(h.(
the_argument_of H)) if len(H)=n+1 & H is ExistGlobal, (the EUntill of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) if len(H)=n+1 & H is
ExistUntill, h.H if len(H) CTLModelStr equals
:: MODELC_1:def 30
CTLModelStr(# {0}, [#]{0}, op2, op1, op1, op1, op2#);
end;
registration
cluster TrivialCTLModel -> with_basic strict non empty;
end;
registration
cluster non empty for CTLModelStr;
end;
registration
cluster with_basic for non empty CTLModelStr;
end;
definition
mode CTLModel is with_basic non empty CTLModelStr;
end;
registration let C be CTLModel;
cluster the BasicAssign of C -> non empty;
end;
reserve V for CTLModel;
reserve Kai for Function of atomic_WFF,the BasicAssign of V;
reserve f,f1,f2 for Function of CTL_WFF,the carrier of V;
definition
let V be CTLModel;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let n be Element of NAT;
func EvalSet(V,Kai,n) ->non empty set equals
:: MODELC_1:def 31
{h where h is Function of
CTL_WFF,the carrier of V : h is-PreEvaluation-for n,Kai};
end;
definition
let V be CTLModel;
let v0 be Element of the carrier of V;
let x be set;
func CastEval(V,x,v0) ->Function of CTL_WFF,the carrier of V equals
:: MODELC_1:def 32
x
if x in Funcs(CTL_WFF,the carrier of V) otherwise CTL_WFF --> v0;
end;
definition
let V be CTLModel;
let Kai be Function of atomic_WFF,the BasicAssign of V;
func EvalFamily(V,Kai) -> non empty set means
:: MODELC_1:def 33
for p being set holds
p in it iff p in bool Funcs(CTL_WFF,the carrier of V) & ex n being Element
of NAT st p=EvalSet(V,Kai,n);
end;
theorem :: MODELC_1:3
ex f st f is-Evaluation-for Kai;
theorem :: MODELC_1:4
f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai implies f1 = f2;
definition
let V be CTLModel;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let H be CTL-formula;
func Evaluate(H,Kai) -> Assign of V means
:: MODELC_1:def 34
ex f being Function of
CTL_WFF,the carrier of V st f is-Evaluation-for Kai & it = f.H;
end;
notation
let V be CTLModel;
let f be Assign of V;
synonym 'not' f for f`;
let g be Assign of V;
synonym f '&' g for f "/\" g;
end;
definition
let V be CTLModel;
let f be Assign of V;
func EX(f) -> Assign of V equals
:: MODELC_1:def 35
(the EneXt of V).f;
func EG(f) -> Assign of V equals
:: MODELC_1:def 36
(the EGlobal of V).f;
end;
definition
let V be CTLModel;
let f,g be Assign of V;
func f EU g -> Assign of V equals
:: MODELC_1:def 37
(the EUntill of V).(f,g);
func f 'or' g -> Assign of V equals
:: MODELC_1:def 38
'not'('not'(f) '&' 'not'(g));
end;
::Some properties of evaluate function of CTL
theorem :: MODELC_1:5
Evaluate('not' H,Kai) = 'not' Evaluate(H,Kai);
theorem :: MODELC_1:6
Evaluate(H1 '&' H2,Kai) = Evaluate(H1,Kai) '&' Evaluate(H2,Kai);
theorem :: MODELC_1:7
Evaluate(EX H,Kai) = EX Evaluate(H,Kai);
theorem :: MODELC_1:8
Evaluate(EG H,Kai) = EG Evaluate(H,Kai);
theorem :: MODELC_1:9
Evaluate(H1 EU H2,Kai) = Evaluate(H1,Kai) EU Evaluate(H2,Kai);
theorem :: MODELC_1:10
Evaluate(H1 'or' H2,Kai) = Evaluate(H1,Kai) 'or' Evaluate(H2,Kai );
:: definition of iteration of function: f|**n
notation
let f be Function;
let n be Nat;
synonym f|**n for iter (f,n);
end;
definition
let S be set;
let f be Function of S,S;
let n be Nat;
redefine func f|**n -> Function of S,S;
end;
reserve S for non empty set;
reserve R for total Relation of S,S;
reserve s,s0,s1 for Element of S;
:: scheme for path with condition F
scheme :: MODELC_1:sch 1
ExistPath{ S()-> non empty set, R()-> total Relation of S(),S(), s0()->
Element of S(), F(Element of S())-> set}: ex f being sequence of S() st f.0
=s0() & for n being Element of NAT holds [f.n,f.(n+1)] in R() & f.(n+1) in F(f.
n)
provided
for s being Element of S() holds Im(R(),s) /\ F(s) is non empty
Subset of S();
:: definition of infinity path
definition
let S be non empty set;
let R be total Relation of S,S;
mode inf_path of R -> sequence of S means
:: MODELC_1:def 39
for n being Nat holds [it.n,it.(n+1)] in R;
end;
::definition of concrete object of CTL model
definition
let S be non empty set;
func ModelSP(S) -> set equals
:: MODELC_1:def 40
Funcs(S,BOOLEAN);
end;
registration
let S be non empty set;
cluster ModelSP(S) -> non empty;
end;
:: definition Fid:ModelSP(S) -> Function of S,BOOLEAN
definition
let S be non empty set;
let f be object; :: zastapic przez In(.,.) ??? !!!
func Fid(f,S) -> Function of S,BOOLEAN equals
:: MODELC_1:def 41
f if f in ModelSP(S)
otherwise S --> FALSE;
end;
::schemes for existence & uniqueness of 1 Operand functor
scheme :: MODELC_1:sch 2
Func1EX{S()->non empty set, f()->Function of S(),BOOLEAN,
F(object,Function of S(),BOOLEAN) -> boolean object}:
ex g being set st g in ModelSP(S()) & for s being
set st s in S() holds F(s,f()) =TRUE iff (Fid(g,S())).s=TRUE;
scheme :: MODELC_1:sch 3
Func1Unique{S()->non empty set, f()->Function of S(),BOOLEAN,
F(object,Function of S(),BOOLEAN) -> boolean object}:
for g1,g2 being set st g1 in ModelSP(S()) & (
for s being set st s in S() holds F(s,f()) =TRUE iff (Fid(g1,S())).s=TRUE ) &
g2 in ModelSP(S()) & (for s being set st s in S() holds F(s,f()) =TRUE iff (Fid
(g2,S())).s=TRUE ) holds g1 = g2;
::schemes for existence & uniqueness of Unary Operation
scheme :: MODELC_1:sch 4
UnOpEX{M()->non empty set, F(object)->Element of M()}:
ex o being UnOp of M()
st for f being object st f in M() holds o.(f) = F(f);
scheme :: MODELC_1:sch 5
UnOpUnique{S,M()->non empty set, F(object)->Element of M()}:
for o1,o2 being UnOp of M() st
(for f being object st f in M() holds o1.f = F(f))
& (for f being object st f in M() holds o2.f = F(f)) holds o1=o2;
::schemes for existence & uniqueness of 2 Operands functor .
scheme :: MODELC_1:sch 6
Func2EX{S()->non empty set, f()->Function of S(),BOOLEAN, g()->Function of S
(),BOOLEAN, F(object,Function of S(),BOOLEAN, Function of S(),BOOLEAN)
-> boolean object}:
ex h being set st h in ModelSP(S()) & for s being set st s in S() holds F
(s,f(),g()) =TRUE iff (Fid(h,S())).s=TRUE;
scheme :: MODELC_1:sch 7
Func2Unique{S()->non empty set, f()->Function of S(),BOOLEAN, g()->Function
of S(),BOOLEAN,
F(object,Function of S(),BOOLEAN, Function of S(),BOOLEAN) ->
boolean object}:
for h1,h2 being set st h1 in ModelSP(S()) & (for s being set st s
in S() holds F(s,f(),g()) =TRUE iff (Fid(h1,S())).s=TRUE) & h2 in ModelSP(S())
& (for s being set st s in S() holds F(s,f(),g()) =TRUE iff (Fid(h2,S())).s=
TRUE) holds h1 = h2;
:: definition of Not_ unary operation of Model Space.
definition
let S be non empty set;
let f be object;
func Not_0(f,S) -> Element of ModelSP(S) means
:: MODELC_1:def 42
for s being set st s
in S holds 'not' (Castboolean (Fid(f,S)).s) = TRUE iff (Fid(it,S)).s = TRUE;
end;
definition
let S be non empty set;
func Not_(S) -> UnOp of ModelSP(S) means
:: MODELC_1:def 43
for f being object st f in ModelSP(S) holds it.f = Not_0(f,S);
end;
:: definition of EneXt_ unary operation of Model Space.
definition
let S be non empty set;
let R be total Relation of S,S;
let f be Function of S,BOOLEAN;
let x be object;
func EneXt_univ(x,f,R) -> Element of BOOLEAN equals
:: MODELC_1:def 44
TRUE if x in S &
ex pai being inf_path of R st pai.0 = x & f.(pai.1) =TRUE otherwise FALSE;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let f be object;
func EneXt_0(f,R) -> Element of ModelSP(S) means
:: MODELC_1:def 45
for s being set st
s in S holds EneXt_univ(s,Fid(f,S),R)=TRUE iff (Fid(it,S)).s=TRUE;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
func EneXt_(R) -> UnOp of ModelSP(S) means
:: MODELC_1:def 46
for f being object st f in ModelSP(S) holds it.f = EneXt_0(f,R);
end;
:: definition of EGlobal_ unary operation of Model Space.
definition
let S be non empty set;
let R be total Relation of S,S;
let f be Function of S,BOOLEAN;
let x be set;
func EGlobal_univ(x,f,R) -> Element of BOOLEAN equals
:: MODELC_1:def 47
TRUE if x in S
& ex pai being inf_path of R st (pai.0 = x & for n being Element of NAT holds f
.(pai.n) =TRUE) otherwise FALSE;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let f be object;
func EGlobal_0(f,R) -> Element of ModelSP(S) means
:: MODELC_1:def 48
for s being set
st s in S holds EGlobal_univ(s,Fid(f,S),R)=TRUE iff (Fid(it,S)).s=TRUE;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
func EGlobal_(R) -> UnOp of ModelSP(S) means
:: MODELC_1:def 49
for f being object st f in ModelSP(S) holds it.f = EGlobal_0(f,R);
end;
:: definition of And_ Binary Operation of Model Space.
definition
let S be non empty set;
let f,g be set;
func And_0(f,g,S) -> Element of ModelSP(S) means
:: MODELC_1:def 50
for s being set st
s in S holds (Castboolean (Fid(f,S)).s ) '&' (Castboolean (Fid(g,S)).s ) =TRUE
iff (Fid(it,S)).s=TRUE;
end;
definition
let S be non empty set;
func And_(S) -> BinOp of ModelSP(S) means
:: MODELC_1:def 51
for f,g being set st f in
ModelSP(S) & g in ModelSP(S) holds it.(f,g) = And_0(f,g,S);
end;
:: definition of EUntill_ Binary Operation of Model Space.
definition
let S be non empty set;
let R be total Relation of S,S;
let f,g be Function of S,BOOLEAN;
let x be set;
func EUntill_univ(x,f,g,R) -> Element of BOOLEAN equals
:: MODELC_1:def 52
TRUE if x in
S & ex pai being inf_path of R st (pai.0 = x & ex m being Element of NAT st (
for j being Element of NAT st j Element of ModelSP(S) means
:: MODELC_1:def 53
for s being set
st s in S holds EUntill_univ(s,Fid(f,S),Fid(g,S),R)=TRUE iff (Fid(it,S)).s=TRUE
;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
func EUntill_(R) -> BinOp of ModelSP(S) means
:: MODELC_1:def 54
for f,g being set st f
in ModelSP(S) & g in ModelSP(S) holds it.(f,g) = EUntill_0(f,g,R);
end;
:: definition of concrete object of CTL model by ModelSP
definition
let S be non empty set;
let X be non empty Subset of ModelSP(S);
let s be object;
func F_LABEL(s,X) -> Subset of X means
:: MODELC_1:def 55
for x being object holds x in it
iff x in X & ex f being Function of S,BOOLEAN st f=x & f.s=TRUE;
end;
definition
let S be non empty set;
let X be non empty Subset of ModelSP(S);
func Label_(X) -> Function of S,bool X means
:: MODELC_1:def 56
for x being object st x in S holds it.x = F_LABEL(x,X);
end;
definition
let S be non empty set;
let S0 be Subset of S;
let R be total Relation of S,S;
let Prop be non empty Subset of ModelSP(S);
func KModel(R,S0,Prop) -> KripkeStr over Prop equals
:: MODELC_1:def 57
KripkeStr (# S, S0, R,
Label_(Prop) #);
end;
registration
let S be non empty set;
let S0 be Subset of S;
let R be total Relation of S,S;
let Prop be non empty Subset of ModelSP(S);
cluster the carrier of KModel(R,S0,Prop) -> non empty;
end;
registration
let S be non empty set;
let S0 be Subset of S;
let R be total Relation of S,S;
let Prop be non empty Subset of ModelSP(S);
cluster ModelSP(the carrier of KModel(R,S0,Prop)) -> non empty for Subset of
Funcs(the carrier of KModel(R,S0,Prop),BOOLEAN);
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
func BASSModel(R,BASSIGN) -> CTLModelStr equals
:: MODELC_1:def 58
CTLModelStr(# ModelSP(S),
BASSIGN, And_(S), Not_(S), EneXt_(R), EGlobal_(R), EUntill_(R) #);
end;
registration
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
cluster BASSModel(R,BASSIGN) -> with_basic non empty;
end;
reserve BASSIGN for non empty Subset of ModelSP(S);
reserve kai for Function of atomic_WFF,the BasicAssign of BASSModel(R,BASSIGN);
:: definition of correctness of Assign of BASSModel(R,BASSIGN)
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let s be Element of S;
let f be Assign of BASSModel(R,BASSIGN);
pred s |= f means
:: MODELC_1:def 59
(Fid(f,S)).s=TRUE;
end;
notation
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let s be Element of S;
let f be Assign of BASSModel(R,BASSIGN);
antonym s |/= f for s |= f;
end;
theorem :: MODELC_1:11
for a being Assign of BASSModel(R,BASSIGN) st a in BASSIGN holds
s |= a iff a in (Label_(BASSIGN)).s;
theorem :: MODELC_1:12
for f being Assign of BASSModel(R,BASSIGN) holds s |= 'not'(f) iff s |/= f;
theorem :: MODELC_1:13
for f,g being Assign of BASSModel(R,BASSIGN) holds s |= f '&' g
iff s|=f & s|=g;
theorem :: MODELC_1:14
for f being Assign of BASSModel(R,BASSIGN) holds s |= EX(f) iff
ex pai being inf_path of R st pai.0 = s & (pai.1) |= f;
theorem :: MODELC_1:15
for f being Assign of BASSModel(R,BASSIGN) holds s |= EG(f) iff
ex pai being inf_path of R st pai.0 = s & for n being Element of NAT holds (pai
.n) |= f;
theorem :: MODELC_1:16
for f,g being Assign of BASSModel(R,BASSIGN) holds s |= f EU g
iff ex pai being inf_path of R st pai.0 = s & ex m being Element of NAT st (for
j being Element of NAT st j Element of S equals
:: MODELC_1:def 61
s0 if n=0 otherwise
pai.(k_nat(k_nat(n)-1));
end;
theorem :: MODELC_1:27
[s0,s1] in R implies ex pai being inf_path of R st pai.0 = s0 & pai.1=s1;
theorem :: MODELC_1:28
for f being Assign of BASSModel(R,BASSIGN) holds s |= EX(f) iff
ex s1 being Element of S st [s,s1] in R & s1 |= f;
:: definition of predecessor
definition
let S be non empty set;
let R be total Relation of S,S;
let H be Subset of S;
func Pred(H,R) -> Subset of S equals
:: MODELC_1:def 62
{ s where s is Element of S : ex t
being Element of S st t in H & [s,t] in R };
end;
:: definition of SIGMA
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f be Assign of BASSModel(R,BASSIGN);
func SIGMA(f) -> Subset of S equals
:: MODELC_1:def 63
{ s where s is Element of S : s|= f };
end;
:: SIGMA is one to one.
theorem :: MODELC_1:29
for f, g being Assign of BASSModel(R,BASSIGN) holds SIGMA(f) = SIGMA(g)
implies f=g;
:: definition of Tau (inverse of SIGMA).
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let T be Subset of S;
func Tau(T,R,BASSIGN) -> Assign of BASSModel(R,BASSIGN) means
:: MODELC_1:def 64
for s being set st s in S holds (Fid(it,S)).s = chi(T,S).s;
end;
:: Tau is one to one.
theorem :: MODELC_1:30
for T1,T2 being Subset of S holds Tau(T1,R,BASSIGN) = Tau(T2,R,BASSIGN
) implies T1=T2;
:: Tau is on to.
theorem :: MODELC_1:31
for f being Assign of BASSModel(R,BASSIGN) holds Tau(SIGMA(f),R, BASSIGN) = f
;
:: SIGMA is on to.
theorem :: MODELC_1:32
for T being Subset of S holds SIGMA(Tau(T,R,BASSIGN)) = T;
:: SIGMA is homomorphism .
theorem :: MODELC_1:33
for f,g being Assign of BASSModel(R,BASSIGN) holds SIGMA('not' f)
= S \ SIGMA(f) & SIGMA(f '&' g) = SIGMA(f) /\ SIGMA(g) & SIGMA(f 'or' g) =
SIGMA(f) \/ SIGMA(g);
:: Tau is monotonic.
theorem :: MODELC_1:34
for G1,G2 being Subset of S holds G1 c= G2 implies for s being
Element of S holds s|= Tau(G1,R,BASSIGN) implies s|= Tau(G2,R,BASSIGN);
:: SIGMA is monotonic.
theorem :: MODELC_1:35
for f1,f2 being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= f1 implies s|= f2) implies SIGMA(f1) c= SIGMA(f2);
:: theorems for translation
:: problem of
:: (1)find status s st s |= EG(f)
:: (2)find status s st s |= f EU g
:: to "find fixpoint of some function of bool S -> bool S".
:: definition Fax(f,*):carrier ->carrier
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f,g be Assign of BASSModel(R,BASSIGN);
func Fax(f,g) -> Assign of BASSModel(R,BASSIGN) equals
:: MODELC_1:def 65
f '&' EX(g);
end;
:: Fax(f,*) is monotonic.
theorem :: MODELC_1:36
for f,g1,g2 being Assign of BASSModel(R,BASSIGN) holds (for s
being Element of S holds s|= g1 implies s|= g2) implies for s being Element of
S holds s|= Fax(f,g1) implies s|= Fax(f,g2);
::commutative
:: Fax(f,*)
:: Assigns ------> Assigns
:: | |
:: SIGMA | | Tau
:: v v
:: bool S -------> bool S
:: SigFaxTau(f,*)
::
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f be Assign of BASSModel(R,BASSIGN);
let G be Subset of S;
func SigFaxTau(f,G,R,BASSIGN) -> Subset of S equals
:: MODELC_1:def 66
SIGMA(Fax(f,Tau(G,R,
BASSIGN)));
end;
:: SigFaxTau(f,*) is monotonic.
theorem :: MODELC_1:37
for f being Assign of BASSModel(R,BASSIGN), G1,G2 being Subset of
S holds G1 c= G2 implies SigFaxTau(f,G1,R,BASSIGN) c= SigFaxTau(f,G2,R,BASSIGN)
;
:: Some tools to treat path.
definition
let S be non empty set;
let R be total Relation of S,S;
let pai be inf_path of R;
let k be Element of NAT;
func PathShift(pai,k) -> inf_path of R means
:: MODELC_1:def 67
for n being Element of NAT holds it.n = pai.(n+k);
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let pai1,pai2 be inf_path of R;
let n,k be Nat;
func PathChange(pai1,pai2,k,n) -> set equals
:: MODELC_1:def 68
pai1.n if n sequence of S means
:: MODELC_1:def 69
for n being Nat holds it.n = PathChange(pai1,pai2,k,n);
end;
theorem :: MODELC_1:38
for pai1,pai2 being inf_path of R, k being Element of NAT holds
pai1.k = pai2.0 implies PathConc(pai1,pai2,k) is inf_path of R;
:: EG(f) is fixpoint of Fax(f,*).
theorem :: MODELC_1:39
for f being Assign of BASSModel(R,BASSIGN), s being Element of S
holds s|= EG(f) iff s|= Fax(f,EG(f));
:: Existence path for fixpoint of Fax(f,*).
theorem :: MODELC_1:40
for g being Assign of BASSModel(R,BASSIGN), s0 being Element of S
st s0 |= g holds (for s being Element of S holds s|= g implies s|= EX(g))
implies ex pai being inf_path of R st pai.0= s0 & for n being Nat
holds pai.In(n,NAT) |= g;
:: EG(f) is the maximum fixpoint of Fax(f,*)
theorem :: MODELC_1:41
for f,g being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= g iff s|= Fax(f,g)) implies for s being Element of S
holds s|= g implies s|= EG(f);
:: definition of TransEG(f)::translated function for EG(f)
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f be Assign of BASSModel(R,BASSIGN);
func TransEG(f) -> c=-monotone Function of bool S, bool S means
:: MODELC_1:def 70
for G being Subset of S holds it.G = SigFaxTau(f,G,R,BASSIGN);
end;
:: fixpoint of TransEG(f)
theorem :: MODELC_1:42
for f,g being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= g iff s|= Fax(f,g)) iff SIGMA(g) is_a_fixpoint_of
TransEG(f);
theorem :: MODELC_1:43
for f being Assign of BASSModel(R,BASSIGN) holds SIGMA(EG(f)) = gfp(S,
TransEG(f));
:: definition Foax(g,f,*):carrier ->carrier
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f,g,h be Assign of BASSModel(R,BASSIGN);
func Foax(g,f,h) -> Assign of BASSModel(R,BASSIGN) equals
:: MODELC_1:def 71
g 'or' Fax(f,h);
end;
:: Foax(g,f,*) is monotonic.
theorem :: MODELC_1:44
for f,g,h1,h2 being Assign of BASSModel(R,BASSIGN) holds (for s
being Element of S holds s|= h1 implies s|= h2) implies for s being Element of
S holds s|= Foax(g,f,h1) implies s|= Foax(g,f,h2);
::commutative
:: Foax(g,f,*)
:: Assigns ------> Assigns
:: | |
:: SIGMA | | Tau
:: v v
:: bool S -------> bool S
:: SigFoaxTau(g,f,*)
::
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f,g be Assign of BASSModel(R,BASSIGN);
let H be Subset of S;
func SigFoaxTau(g,f,H,R,BASSIGN) -> Subset of S equals
:: MODELC_1:def 72
SIGMA(Foax(g,f,Tau(H,
R,BASSIGN)));
end;
:: SigFoaxTau(g,f,*) is monotonic.
theorem :: MODELC_1:45
for f,g being Assign of BASSModel(R,BASSIGN), H1,H2 being Subset
of S holds H1 c= H2 implies SigFoaxTau(g,f,H1,R,BASSIGN) c= SigFoaxTau(g,f,H2,R
,BASSIGN);
:: f EU g is fixpoint of Foax(g,f,*).
theorem :: MODELC_1:46
for f,g being Assign of BASSModel(R,BASSIGN), s being Element of
S holds s|= f EU g iff s|= Foax(g,f,f EU g);
:: f EU g is the minimum fixpoint of Foax(g,f,*)
theorem :: MODELC_1:47
for f,g,h being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= h iff s|= Foax(g,f,h)) implies for s being Element of S
holds s|= f EU g implies s|= h;
:: definition of TransEU(f,g)::translated function for f EU g
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f,g be Assign of BASSModel(R,BASSIGN);
func TransEU(f,g) -> c=-monotone Function of bool S, bool S means
:: MODELC_1:def 73
for H being Subset of S holds it.H = SigFoaxTau(g,f,H,R,BASSIGN);
end;
:: fixpoint of TransEU(f,g)
theorem :: MODELC_1:48
for f,g,h being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= h iff s|= Foax(g,f,h)) iff SIGMA(h) is_a_fixpoint_of
TransEU(f,g);
theorem :: MODELC_1:49
for f,g being Assign of BASSModel(R,BASSIGN) holds SIGMA(f EU g) = lfp(
S,TransEU(f,g));
:: Solver for EX and TransEG,TransEU
theorem :: MODELC_1:50
for f being Assign of BASSModel(R,BASSIGN) holds SIGMA(EX(f)) =
Pred(SIGMA(f),R);
theorem :: MODELC_1:51
for f being Assign of BASSModel(R,BASSIGN), X being Subset of S holds (
TransEG(f)).X = SIGMA(f) /\ Pred(X,R);
theorem :: MODELC_1:52
for f,g being Assign of BASSModel(R,BASSIGN), X being Subset of S holds
(TransEU(f,g)).X = SIGMA(g) \/ (SIGMA(f) /\ Pred(X,R));