:: Model Checking, Part {I} :: by Kazuhisa Ishida :: :: Received November 14, 2006 :: Copyright (c) 2006-2021 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));