Representing RCC relations in temporal logic
Contents
1. 14 Y DC X Y 2 y DAX Y VWEC X Y 2 y 0 2 0X y OY yO AX Y YPO X Y 2 OU OX YY 2 y AX AAV 20 O6X Y VWEQ X Y 2 DAX v Y x y AX v Y YTPP X Y 2 YDGX v Y NOA a gt y OY YNTPP X Y x y LY X v y OY Making a distinction between temporal players and spatial players makes it possible to represent both temporal and spatial information in a transition system Figure 5 gives an example of how this is done Every node in the tem poral transition system is replaced with the set of nodes of the spatial transition system These nodes are connected for the spatial player In the example these are qo q and q2 All these nodes are connected for the temporal player with the node on the same location in the next state In the example a few of these connections are represented by dotted lines do qi q2 Figure 5 The representation of three temporal states in ATL 5 Parking example In this example we show how the combination of ATL and RCC can be used to reason about parking fees There are often different parking zones in a city with 15 different rates These rates can also change over time We will give a fictional city with parking zones and changing rates Within this example we will try to answer some questions like in what regions you can park for what rates Figure 6 shows a map of the fictional ci2. PP X Y 3z EC Z X EC Z Y PUX Y P Y X PP I X Y PP Y X TPP X Y TPP Y X NTPP X Y NTPP Y X DC X Y stands for X is disconnected from Y P X Y stands for X is part of Y PP X Y stands for X is a proper part of Y EQ X Y stands for X is equivalent to Y O X Y stands for X overlaps Y PO X Y stands for X partially overlaps Y DR X Y stands for X is discrete from Y TPP X Y stands for X is a tangential proper part of Y EC X Y stands for X is externally connected with Y NTPP X Y stands for X is a non tangential proper part of Y For the inverse of the notation is used where e P PP TPP NTPP In this article we will use RCC8 RCCS only uses the relations DC EC PO EQ TPP NTTP TTP and NTTP A visual representation of these relations is shown in Figure 3 2In 9 X Y is used instead of EQ X Y 5 y 6 e DC X Y PO X Y TPP X Y TPP X Y EC X Y EQ X Y NTPP X Y NTPP X Y Figure 3 A visual representation of the RCC8 relations There is a distinction between the interior and the boundary of a region The interior of y is denoted zy Looking at Figure 3 it is easy to see that the RCCS relations can also be defined with the following set formulas DC X Y XnY 9 EC X Y XnY 4oO iXniY 9o PO X Y X Y AY XniXuiY o EQ X Y X Y TPP X Y XcYAX iY NTPP X Y XciY Modal Logics for Qualitative Spatial Reasoning 5 gives a trans
3. II is the finite set of atomic propositions is the labelling function For each state q Q a set l q II of propositions is true at q A definition of ATL is given in the article Alternating time temporal logic 3 For every temporal operator a set of players is given It is defined in the following grammar where pe Il and A Y ex Tltlp pl pr apa lr y exi AO PI MAD MAJO pl A veiut Lar a1 can be written as a1 a1 and 2 can be written as A is defined as A p The intuitive meaning of the boolean operators is the same as in proposition logic The intuitive meaning of A v is that the set of players A can cooperate to make y true The intuitive meaning of A v is that the set of players A cannot avoid to make y true The temporal operators have the following intuitive meanings A L e means players A can cooperate to make y always hold A v means players A can cooperate to make y eventually hold A Oy means players A can cooperate to make hold in the next state A vitqo means players A can cooperate to make 4 hold until p2 holds To give the semantic definition of ATL we first define the notion of strategies A strategy for player a gt is the function fa Given a nonempty finite state sequence A Q the function fa gives a natural number such that f A x d q where q is the last state of A We write Fa fala A for the set of strategies of the players in A We define out
4. O q gt p false q gt p true module B is interface q bool external p bool atom contq controls q reads p init true gt q true update p gt q false p gt q true Figure 2 How a model is represented in Mocha 4 Spatial reasoning Now that we have defined LTL CTL and ATL and described model checkers for these temporal logics we want to represent spatial information with these temporal logics Every temporal step between states can be seen as a step in spatial space What can be expressed with the temporal logics is however not very useful for spatial reasoning That is why we represent RCC with the temporal logics First we will define RCC and then we try to represent it with the temporal logics 4 1 Region Connection Calculus RCC is a way to represent relations between regions The definition for RCC is based on the C X Y relation which means X connects with Y 9 Where X and Y are spatial regions This relation is reflexive and symmetric thus X is connected with itself and if X is connected with Y then is Y connected with X All other relations are defined with C z y in the following way DC X Y C X Y P X Y Vz C Z X gt C Z Y PP X Y P X Y P Y X EQ X Y P X Y AP Y X O X Y 3z P Z X AP Z Y PO X Y O X Y A P X Y A P Y X DR X Y O X Y TPP X Y PP X Y 3z EC Z X EC Z Y EC X Y C z y O X Y NTPP X Y
5. Vy is pronounced y is inevitable and means that in every future y holds at some point 3 lt gt p is pronounced holds potentially and means that there is a future where y holds at some point V is pro nounced invariantly y and means that in all futures y always holds 30y is pronounced potentially always y and means that there is a future where y always holds V Oy is pronounced for all paths next y and means that in all futures y holds in the next stats 3O is pronounced for some path next y and means that there is a future where y holds in the next state WU pa is pronounced for all paths y until y2 and means that in all futures y holds until pa holds 4y Uye2 is pronounced for some path y until y2 and means that there is a future where y holds until pa holds Now we give the semantic definition of CTL A tree 7 is an infinite set of states Every state is a set of the atomic propositions that are true in this state The first state of the tree is the root r Every state is connected with other states which are called it s children There are no cycles in the tree 7 satisfies an LTL formula y if TE y The function p 7 gives a set of all possible paths on tree m A path is possible when Ao r and A 1 is a child of A The relation has the following properties T RET am KL T ED iffper T Ep iff 7 yp TEPNY iff r pando E v TEPVY ifreporey T amp Jo iff T E o for some e
6. but also when they partially overlap The temporal 17 lt gt operator is again used for translating there is a moment The formula for this question becomes EC Centre 0 v PO Centre 0 or in ATL days OU Neon city Centre zone L10 city zone yO city L Center zone L0 city zone Q Centre 0 We already know that you can never park in the Centre for free Meaning there is no partial overlap between the centre and a free parking zone But there is a moment when the Centre and a free parking zone are externally connected Namely on Sunday you can park for free just east and just west of the Centre There is a moment when you can park for free next to the Centre 6 Conclusion In this article we asked whether RCC relations could be represented into a temporal logic and whether this could be done in such a way that the spatial regions and the temporal relations can be used like in a spatio temporal logic We have found that LTL can only represent the RCC relations DC EQ and NTPP We found that CTL can represent all the RCC relations but it is not possible to also use temporal relations We found that in ATL both the spatial RCC relations and temporal relations can be used like in a spatio temporal logic This is possible by making a distinction between temporal and spatial players We wanted to represent a spatial logic into a temporal logic so that the existing model checker for the temp
7. jMocha can only do invariant and refinement checking Invariant checking can only check formulas of the form A LIe where y doesn t contain any other temporal operators Nesting temporal operators is not possible Refinement checking is checking whether the traces generated by one model is a subset of the traces generated by another model Giving a model to Mocha is not as simple as it is in MCheck A set of variables is given instead of a set of states Each possible combination of values of the variables is a state The transitions between the states are given by allowing each player to only change certain variables Each variable can only be controlled by one player The strategy of the player is given by formulas that assign values to the variables These formulas can use variables controlled by other players Every game structure can be represented in this way but the translation isn t always straightforward Figure 2 gives an example of how models are represented in Mocha lInstalling cMocha on Linux gave the following problems tcl version 8 6 doesn t work with Tix version 8 4 3 The code in until h has obj 0 instead of obj 0 line 175 and 185 File invMain c gives and error line 127 The file configure of mocha 1 0 1 has an apostrophe to much line 850 File prsLex c gives an error line 1527 module A is interface p bool external q bool atom contp controls p reads q init true gt p true update
8. P r T EVD iff T E y for allr e P r TEOY iff 3j gt 0O r j EY T EF le iff Vj gt 0 r j Ey T EO iff r 1 p T EQU iff 3j 2 0 7 j v and V0 k lt j T k e p Here 7 j gives a tree with the jst state in the path 7 as the root of the tree The semantics of CTL don t have to be in terms of trees but can also be given in terms of transition systems A tree in transition system T Q qo 9 11 1 has it s root at go and Vi 2 0 has children qi j for all j from 1 to d q 2 3 Alternating time Temporal Logic ATL is a logic that makes it possible to reason about time with multiple agents ATL uses a transition system similar to the one used for LTL and CTL called a game structure 3 A game structure has multiple players this makes it possible to reason with multiple agents A game structure is a tuple S k Q qo IL L Where k e N is the number of players and k gt 1 We write 1 k for the set of players Q is the set of states qo Q is the initial state When q Q and j1 jx D q then 0 q j1 jx Q is a transition function Where D a is a set of possible move vectors A move vector at q is a tuple j1 jk such that 1 lt ja da q da q is the number of possible transitions in q for player a Y There is a transition between q and q j1 jx if the players can choose moves so that j1 jx D q In each state there is at least one transition possible
9. will hold in the next state qilfq is pronounced pj until y2 and means y will hold until p2 holds Now we give the semantic definition of LTL A path 7 is an infinite line of connected states A with gt 0 Ap is the starting point of the path Every state is a set of atomic propositions that are true in the state T satisfies an LTL formula y if r y Where the E relation has the following properties T ET TEL TEP iff pe Ao TE AY iff TE o TE PAW iff rE pandT E v TEQVY fire porrey TE OY iF3j gt 0 7 5 p T EDO iff vj 20 7 j v T E OQ iff T 1 9 T glti iff 3j 20 7 j e v and 7 i p forall x i j Where r i is the path 7 without the first i states The starting point is then A Note that for Oy the formula y must only hold in the state Ai but to verify this the whole path 7 1 must be given when contains temporal operators the whole path is needed to verify q The semantics of LTL don t have to be in terms of paths but can also be given in terms of transition systems A transition system is a tuple T Q 40 9 11 1 Where Q is a set of states qo Q is the initial state When qeQ and 0 j d q then q j Q is a transition function Where d q is the number of possible transitions in q There is a transition between q and 6 q j and in each state there is at least one transition possible We identify the transitions with the number j II is the finite set of atomic p
10. 2 713 2002 Christel Baier Joost Pieter Katoen et al Principles of model checking volume 26202649 MIT press Cambridge 2008 Brandon Bennett Modal logics for qualitative spatial reasoning Logic Journal of IGPL 4 1 23 45 1996 Roman Kontchakov Agi Kurucz Frank Wolter and Michael Za kharyaschev Spatial logic temporal logic In Handbook of spatial logics pages 497 564 Springer 2007 Werner Nutt On the translation of qualitative spatial reasoning problems into modal logics In K1 99 Advances in Artificial Intelligence pages 113 124 Springer 1999 Amir Pnueli The temporal logic of programs In Foundations of Computer Science 1977 18th Annual Symposium on pages 46 57 IEEE 1977 David A Randell Zhan Cui and Anthony G Cohn A spatial logic based on regions and connection KR 92 165 176 1992 Jeff Sember Mcheck A model checker for ltl and ctl formulas 2005 19
11. L we can represent set constraints in the following way B s T VO s B s 1 VO B s Bls FT O b s B s 1 IOB 5 Using on the RCC set expressions gives the following result 13 B DC X Y VOA X Y B EC X Y YO YOX YOY IO X AY B PO X Y IO VOX YDY 3O X Y 3O XAY B EQ X Y VO AX VY VO X v Y B TPP X Y VOGXvY A A X AVOY B NTPP X Y VO X v VOY We now have a representation of RCC8 in CTL However the representation of regions in the transition system makes temporal reasoning not possible There is no distinction between temporal transitions and spatial transitions We need to make a distinction between temporal and spatial operators 4 4 Representing RCC in ATL Just like in CTL RCC can be represented in ATL But we can make a distinction between temporal and spatial operators by making a distinction between players for temporal reasoning and players for spatial reasoning y maps every set expression formula to an ATL formula in the following way yi 1 yt T y snt ys ay t y sut y s v y t y s 1 s y Is As 0y s As is the set of players active in s Set constraints are represented in the following way vs T As Ov s vs 1 ALI 9 vs FT As 9 vs 1 AJ O 1 s Using y on the RCC set expressions gives the following result where region X is defined by player x and region Y by player y
12. Representing RCC relations in temporal logic Author Supervisor Tim Harteveld Dr ir Jan Broersen January 30 2015 15 ECTS Abstract In this article we attempt to represent a spatial logic with a temporal logic in such a way that the spatial relations and the temporal relations can be used like a spatio temporal logic The spatial logic we try to represent is the Region Connection Calculus RCC The temporal logics we will discuss are Linear time Temporal Logic LTL Computation Tree Logic CTL and Alternating time Temporal Logic ATL We also discuss the available model checkers for these temporal logics and give an example of the use of the spatio temporal logic We conclude that LTL can only represent some RCC relations CTL can represent all RCC relations but temporal reasoning isn t possible anymore ATL can represent all RCC relations and temporal reasoning is still possible Contents 1 2 Introduction 2 Temporal logics 2 2 1 Linear time Temporal Logic o ooo o 2 2 2 Computation Tree Logic o oo e 3 2 3 Alternating time Temporal Logic ooo 5 Model checking 6 Jul MO b c ato pad ana aaa a 6 3 2 Mocha A etum VENE Ra EU eu 7 Spatial reasoning 9 4 1 Region Connection Calculus o oo o 9 4 2 Representing RCC in LTL ooo oo 12 4 3 Representing RCC in CTL o o o ooo ooo ooo o 13 4 4 Representing RCC in ATL co ooo
13. er There are many model checkers for LTL and CTL but there are not many model checkers for ATL The only model checker for ATL we are aware of is called Mocha In section 3 1 we give a description of a model checker for LTL and CTL In section 3 2 we give a description the model checker Mocha for ATL 3 1 MCheck MCheck 10 is a simple model checker for LTL and CTL The program is a JAR file This makes it easy to implement in java programs and nothing needs to be installed MCheck has no GUI interface but is still simple to use The command mch test txt will verify the LTL and CTL formulas given in test txt for the model given in test txt A model is given by writing for each state the name followed by the states to which the state has transitions and the propositions that are true in the state The initial state is indicated with gt before the name of the state Figure 1 gives an example of how models are represented in MCheck The LTL and CTL formulas are written as expected where the temporal operators are given with capital letters p q p a p aq ip q b0 012 pq 1 12 q 23 3 30 p Figure 1 How a model is represented in MCheck 3 2 Mocha There are two versions of Mocha cMocha 2 and Mocha 1 cMocha is the first version and is mostly written in C Mocha is the second version and is mostly written in Java On Windows Mocha didn t fully work on Linux it did cMocha didn t work at all
14. id of states Typically a lot more states are used but for the clarity of this example we used the minimal number of states necessary It is also not required for the states to be in a grid 11 OO Oc Oc OO OO cQ los Lamina bona leva dz iu OG ESOO DO X MX LAN ADAN ZZ Z a a a em e C AC alo dv br lol ESOO LO Or OO O OOOO O Figure 4 Example of three regions represented in a spatial transition system 4 2 Representing RCC in LTL Now that we have set expressions for the RCCS relations we can try to give a translation from these set expressions to LTL formulas The function makes this translation by mapping every set expression to an LTL formula in the following way a 1 1 a t T a snt a s o t a sut a s va t a s a s a Is la s Most of these mappings are very straightforward The mapping of the S4 operator a Is to la s isn t directly obvious I is a 4 operator equivalent to the J operator in a S4 frame LTL is a reflexive and transitive and thus has a S4 frame Because LTL is 4 a Is can be mapped to Ha s We now have a translation from set expressions to LTL formulas However the translation from set constraints to LTL formulas with the functions a gives a problem The translation from s T to s must hold everywhere in the universe is simple to do with the operator This translation is given below B
15. ions are defined in their usual way Te s tiff d s d s Te s tiff d s d s Now we can rewrite the RCC relations from set formulas into the set expres sions DC X Y XnY 1 EC X Y XnY 1 IXnIY 2 1 PO X Y IXnIY 1 XnY 1 XnY 1 EQ X Y X Y TPP X Y X MY E i a XnIY S NTPP X Y XnIY 1 The temporal logics LTL CTL and ATL are not continues they are based on transitions systems This means that the spatial regions used in RCC must also be represented in a transition system T Q qo 0 IL l that we call spatial transition system The universe U will be the set of all states Q qo is a state that s not part of any region 6 is the reachability between states typically if two states are next to each other in the spatial space then they are connected in both ways A region will be a set of states where a certain proposition is true The distinction between the interior and the boundary of a region is made with the reachability of states The interior has no transitions to states outside the interior This makes it possible to say that something holds inside the interior of are region with the expression it holds in all reachable states starting inside the region Figure 4 gives an example of a spatial transition system Dotted lines show which part of the transition system corresponds to the regions The set of true propositions are given for each state The regions are represented in a five by nine gr
16. lation from RCC constraints to multimodal propositional logic We want a translation from RCC constraints to LTL CTL and ATL On the Translation of Qualitative Spa tial Reasoning Problems into Modal Logics 7 gives a proof for the translation to multimodal propositional logic I m using a similar proof for the translation to the temporal logics We give a formal language called set expression It is easier to use set expressions for our purposes then the set formulas given above Set expressions s and t are with the following grammar X Y and Z denote the countable infinite set of variables s t X T L sut snt s Is Elementary set constraints have the form s t or s t More complex set constraints can be constructed using the propositional connectives conjunction disjunction and negation If S and T are set constraints then so are SAT SvT and aS 10 The function d maps every set expression to a subset of a topological space A topological space consist of a universe U and a set of subset of U d maps every set expression to a subset of U in the following way d 1 d T U d snt d s nd t d sut d s ud t d s U ds d Is i d s A topological interpretation Z is a triple Z U i d We write Z C if topological interpretation Z satisfies a set constraint C The topological in terpretation for elementary constraints is defined as below The conjunction disjunction and negation in complex topological interpretat
17. near time Temporal Logic LTL Computation Tree Logic CTL and Alternating time Temporal Logic ATL In section 2 we define the temporal logics LTL CTL and ATL In section 3 we discuss some of the available model checkers for these temporal logics In section 4 we define RCC and we try to represent RCC in LTL CTL and ATL In section 5 we give an example In this example we show how the representation of RCC in a temporal logic can be used in a parking scenario In section 6 we conclude this article and formulate an answer to our research questions 2 Temporal logics 2 1 Linear time Temporal Logic LTL is introduced in The temporal logic of programs 8 It is a logic where time is represented as a single path A definition of LTL is given in Principles of model checking 4 The syntax of LTL consists of atomic propositions II the standard boolean operators and temporal operators It is defined with the following grammar where p II e z T L pl 9l ep y ply n val Ov De Ov vites The precedence of the unary operators is equally strong The unary oper ators take precedence over the binary operators The operators and v are equally strong and U is stronger The intuitive meaning of the boolean operators is the same as in proposition logic Oy is pronounced globally y and means y will always hold lt gt g is pro nounced finally y and means that y eventually will hold Op is pronounced next y and means y
18. ooo 14 Parking example 15 Conclusion 18 1 Introduction A lot of reasoning in artificial intelligence is based on logic Logics about time are called temporal logics They make it possible to reason about time Logics about space are called spatial logics They make it possible to reason about space Combining these two logics into a spatio temporal logic makes it possible to reason about space changing over time 6 This makes it possible to reason about situations that involve both temporal and spatial aspects In this article we want to represent spatial relations in a temporal logic In this way the existing model checkers for the temporal logic can be used to reason about both time and space The spatial relation we want to represent in a temporal logic is the Region Connection Calculus RCC RCC makes it possible to reason about relations between spatial regions It can be translated to propositional modal logic 5 We want to translate it into a modal temporal logic This gives us the following research questions Can the RCC relation be represented into a modal temporal logic Can this be done in such a way that the spatial relations and the temporal relations can be used like a spatio temporal logic We are going discuss three different temporal logics to see which one is most suited for the translation of RCC We will also discuss the available model check ers for these temporal logics The temporal logics we will discuss are Li
19. oral logic could be used However there is only one model checker for ATL we are aware of and it s difficult to use and install There are a lot more model checkers for LTL and CTL available A model checker for CTL could be used to check RCC models Because the model checker for ATL is difficult to use it might be better to develop a spatio temporal model checker instead of using an existing temporal model checker In this article we only discussed RCC as the spatial logic Future research could focus on representing other spatial logics into temporal logics Future research could also focus on other temporal logics to represent the spatial logics In artificial intelligence temporal logics is used to reason about time and spatial logics to reason about space In this article we combined some of these temporal and spatial logics into a spatio temporal logic Making it possible to reason about space changing over time like in the given parking example 18 References 1 R Alur H Anand F Ivanci M Kang M McDougall BY Wang L de Al faro TA Henzinger B Horowitz R Majumdar FYC Mang C Meyer Krisch M Minea S Qadeer SK Rajamani and JF Raskin MOCHA user manual Jmocha version 2 0 R Alur L De Alfaro Th A Henzinger SC Krishnan FYC Mang S Qadeer SK Rajamani and S Tasiran MOCHA user manual Rajeev Alur Thomas A Henzinger and Orna Kupferman Alternating time temporal logic Journal of the ACM JACM 49 5 67
20. q FA to be the state sequence followed when q is the initial state and all players in A follow their strategies in F4 thus A is out q Fa if q qo and for all positions i gt 0 there is a move vector 1 Jx D qi such that ja f A 0 4 for all players a A and qi j1 jk Qist Now we can give the definition of the semantics of ATL A state q satisfies an ATL formula y if q y The E relation has the following properties q ET quei q ep iff p e l q q EP iff q p qEpaw if q yandq E q pyy ifqrporqry q A oo iff there exists a set F4 such that for all A out q Fa there is a 4 gt 0 such that A p q EA de iff there exists a set F4 such that for all A out q Fa and all positions gt 0 we have A i y q AJOY iff there exists a set F4 such that for all A out q Fa we have A 1 p q A pU v iff there exists a set F4 such that for all A out q Fa there exists a position gt 0 such that A pa and for all positions 0 lt j i we have A j 1 3 Model checking A model checker is a program that given a model can answer questions about that model For LTL and CTL a model checker can check whether an LTL or CTL formula is true or false given a certain transition system A model checker for ATL can check whether an ATL formula is true or false given an game structure Model checking for LTL and CTL is often combined into a single model check
21. ropositions l is the labelling function For each state q Q a set l q II of propositions is true at q An LTL formula must hold for every path in a transition system A path in a transition system is an infinite sequence of states qo q1 such that Vi gt 0 qi j qui for some 0 lt j x d q The LTL formula must hold for all possible paths of a given transition system 2 2 Computation Tree Logic CTL is a logic where time is represented as a tree At every node there is a choice between different actions which lead to different futures Adding path quantifiers to LTL gives CTL CTL is a fragment of CLT where a path operator must be followed with a temporal operator A definition of CTL is given in Principles of model checking 4 With path quantifiers you can reason with different futures of paths 3 means there exists a path where y holds and V means that y must hold on all paths It is defined with a finite set of propositions II in the following grammar where p II e Tl i pl elvive2 ei val3v Vv V Ov De lOvelveites The precedence fore CTL is the same as for LTL The precedence of the unary operators is equally strong The unary operators take precedence over the binary operators The operators and v are equally strong and UY is stronger The intuitive meaning of the boolean operators is the same as in proposition logic The temporal operators always come in pairs They have the following intuitive meanings
22. s question becomes lt gt PO Centre 0 or in ATL days Qo city zone q city Centre zone EL10 city zone Centre 20 city zone 4 Centre 0 It is possible to park for free in the Centre at any moment On every day there is a parking fee for all the zones that overlap the Centre region Can you park in South with rate B for two days Just like with the previous question if we want to know whether we can park in a region for a certain rate we only have to check whether the region and the zone partially overlap But now we want to check it for the current state and the next We can check the next state using the temporal O operator The formula for this question becomes PO South B OPO South B or in ATL gt city OSouth zone C1B South 5B O South B Q city L1South zone C1B South 5B O South B city zone city zone city zone days O city zone A Zu Zu zu TAA xw x x Wem city zone A x city zone We start on a weekday as shown in Figure 7 It is possible to park in South for rate B on every weekday and on Saturday You can park in South for two days with rate B Is there a moment when you can park for free next to the Centre If you can park for free next to the Centre then there must be a free parking zone just outside of the Centre region This is the case when the region and the zone are externally connected
23. ty and names the different regions in the city There are different parking zones with different parking fees in the city There is a rate A B and C We denote free parking with 0 The rates differ for weekday Saturdays and Sunday s Figure 7 shows the transition system for this situation and the rates for the different zones and the different days Figure 6 The city layout Figure 7 The parking zones and there rates We now want to represent some questions about the parking in this city in ATL formula s To do this we use the following players The temporal player is called days the spatial player for the city regions city and the spatial player for 16 the parking zones zone When the questions are translated to ATL formula s we can use a model checker to get the answer Is there a moment when I can park in the Centre for free It is possible to park in the Centre for free if the Centre region overlaps with a zone with rate 0 There is a moment can be translated with the temporal lt gt operator Note that if we want to know whether we can park in a region for a certain rate we only have to check whether the region and the zone partially overlap We don t have to check whether the zone and the region are equivalent or are some proper part of each other because in this example there are no zones and regions that are equivalent or are a proper part of each other The formula for thi
24. ut translating s T to there is a point in the universe where s doesn t hold is not possible The lt gt operator seems like a good option but lt gt y means on every path y eventually holds and not there is a path where y eventually holds a s T la s a s 1 a s 12 We can only translate set constraints where 7 is not used Only the RCC set expressions DC EQ and NTPP don t use 7 Using the set expressions of these RCC relations gives the following result a DC X Y OA X Y o EQ X Y O XvY A O X v AY a NTPP X Y O X v OY LTL can only represent the RCC relations DC EQ and NTPP and not all RCC8 relations This is because in LTL the formulas must hold for all paths A formula that holds for some paths cannot be represented in LTL but can be represented in CTL 4 3 Representing RCC in CTL We will show that in CTL you can represent RCC The proof is similar to the one given for LTL but now we can represent formulas that hold for some paths The function 8 maps every set expression formula to a CTL formula in the following way Pl 1 B T T B snt B s B t B sut B s v B t B s 8 s B Is VO s Just like with LTL the S4 operator Is is translated with the operator It is translated to VL 18 s because s must hold everywhere in the region Because there are no transitions from the interior of a region to the outside s must always hold on all paths In CT
Download Pdf Manuals
Related Search