hierarchy.org 24 KB
 Alexandre Duret-Lutz committed Jan 12, 2017 1 2 3 # -*- coding: utf-8 -*- #+TITLE: Exploring the temporal hierarchy of Manna & Pnueli #+DESCRIPTION: Spot command-line tools for exploring the temporal hierarchy of Manna & Pnueli  Alexandre Duret-Lutz committed Jun 27, 2018 4 #+INCLUDE: setup.org  Alexandre Duret-Lutz committed Jan 12, 2017 5 #+HTML_LINK_UP: tools.html  Alexandre Duret-Lutz committed Apr 17, 2019 6 #+PROPERTY: header-args:sh :results verbatim :exports both  Alexandre Duret-Lutz committed Jan 12, 2017 7 8  /A hierarchy of temporal properties/ was defined by Manna & Pnueli in  Alexandre Duret-Lutz committed Aug 17, 2017 9 their [[ftp://www-cs.stanford.edu/cs/theory/amir/hierarchy.ps][PODC'90 paper]].  Alexandre Duret-Lutz committed Jan 12, 2017 10 11 12 13 14 15 16 17 18  This hierarchy relates "properties" (i.e., omega-regular languages) to structural properties of the automata that can recognize them. * Description of the classes The hierarchy is built from the classes pictured in the following diagram, where each class includes everything below it. For instance, the /recurrence/ class includes the /obligation/ class which also  Alexandre Duret-Lutz committed Aug 17, 2017 19 20 includes the /safety/ and /guarantee/ classes, as well as the unnamed intersection of /safety/ and /guarantee/ (=B= in the picture).  Alexandre Duret-Lutz committed Jan 12, 2017 21   Alexandre Duret-Lutz committed Nov 22, 2017 22 [[file:hierarchy.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 23 24 25 26  Forget about the LTL properties and about the red letters displayed in this picture for a moment.  Alexandre Duret-Lutz committed Aug 17, 2017 27 28 29 - The /reactivity/ class represents all possible omega-regular languages, i.e., all languages that can be recognized by a non-deterministic Büchi automaton.  Alexandre Duret-Lutz committed Jan 12, 2017 30   Alexandre Duret-Lutz committed Aug 17, 2017 31 32 - The /recurrence/ subclass contains all properties that can be recognized by a deterministic Büchi automaton.  Alexandre Duret-Lutz committed Jan 12, 2017 33   Alexandre Duret-Lutz committed Aug 17, 2017 34 - The dual class, /persistence/ properties, are those that can be  Maximilien Colange committed Aug 28, 2017 35  recognized by a weak Büchi automaton (i.e., in each SCC either all  Alexandre Duret-Lutz committed Aug 17, 2017 36  states are accepting, or all states are rejecting).  Alexandre Duret-Lutz committed Jan 12, 2017 37   Alexandre Duret-Lutz committed Aug 17, 2017 38 39 40 - The intersection of /recurrence/ and /persistence/ classes form the /obligation/ properties: any of those can be recognized by a weak and deterministic Büchi automaton.  Alexandre Duret-Lutz committed Jan 12, 2017 41   Alexandre Duret-Lutz committed Aug 17, 2017 42 43 44 - /Guarantee/ properties are a subclass of /obligation/ properties that can be recognized by terminal Büchi automata (i.e., upon reaching an accepting state, any suffix will be accepted).  Alexandre Duret-Lutz committed Jan 12, 2017 45   Alexandre Duret-Lutz committed Aug 17, 2017 46 - /Safety/ properties are the dual of /Guarantee/ properties: they can  Maximilien Colange committed Aug 28, 2017 47  be recognized by ω-automata that accept all their runs (i.e., the  Alexandre Duret-Lutz committed Aug 17, 2017 48  acceptance condition is "true"). Note that since these automata are  Maximilien Colange committed Aug 28, 2017 49  not necessary complete, it is still possible for some words not to  Alexandre Duret-Lutz committed Aug 17, 2017 50 51 52 53  be accepted. If we interpret the ω-automata with "true" acceptance as finite automata with all states marked as final, we obtain monitors, i.e., finite automata that recognize all finite prefixes that can be extended into valid ω-words.  Alexandre Duret-Lutz committed Jan 12, 2017 54   Maximilien Colange committed Aug 28, 2017 55 - Finally, at the very bottom is an unnamed class that contains  Alexandre Duret-Lutz committed Aug 17, 2017 56 57 58  /Safety/ properties that are also /Guarantee/ properties: those are properties that can be represented by monitors in which the only cycles are self-loops labeled by true.  Alexandre Duret-Lutz committed Jan 12, 2017 59 60 61  The "LTL normal forms" displayed in the above figure help to visualize the type of LTL formulas contained in each of these class. But note  Alexandre Duret-Lutz committed Aug 17, 2017 62 that (1) this hierarchy applies to all omega-regular properties, not  Alexandre Duret-Lutz committed Jan 12, 2017 63 64 65 66 67 68 69 70 71 72 just LTL-defined properties, and (2) the LTL expression displayed in the figure are actually normal forms in the sense that if an LTL-defined property belongs to the given class, then there exists an equivalent LTL property under the stated form, were $p$, $q$, $p_i$ and $q_i$ are subexpressions that may use only Boolean operators, the next operator ($\mathsf{X}$), and past-LTL operators (which are not supported by Spot). The combination of these allowed operators only makes it possible to express constraints on finite prefixes. /Obligations/ can be thought of as Boolean combinations of /safety/  Alexandre Duret-Lutz committed Jul 21, 2020 73 and /guarantee/ properties, while /reactivity/ properties are Boolean  Alexandre Duret-Lutz committed Jan 12, 2017 74 75 76 77 78 79 80 81 82 83 84 85 86 combinations of /recurrence/ and /persistence/ properties. The negation of a /safety/ property is a /guarantee/ property (and vice-versa), and the same duality hold for /persistence/ and /recurrence/ properties. The red letters in each of these seven classes are keys used in Spot to denote the classes. * Deciding class membership The =--format=%h= option can be used to display the "class key" of the most precise class to which a formula belongs.  Alexandre Duret-Lutz committed Apr 17, 2019 87 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 88 89 90 91 92 93 94 95 ltlfilt -f 'a U b' --format=%h #+END_SRC #+RESULTS: : G If you find hard to remember the class name corresponding to the class keys, you can request verbose output with =%[v]h=:  Alexandre Duret-Lutz committed Apr 17, 2019 96 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 97 98 99 100 101 102 103 104 105 ltlfilt -f 'a U b' --format='%[v]h' #+END_SRC #+RESULTS: : guarantee But actually any /guarantee/ property is also an /obligation/, a /recurrence/, a /persistence/, and a /reactivity/ property. You can get the complete list of classes using =%[w]h= or =%[vw]h=:  Alexandre Duret-Lutz committed Apr 17, 2019 106 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 107 108 109 110 111 112 113 114 115 ltlfilt -f 'a U b' --format='%[w]h = %[vw]h' #+END_SRC #+RESULTS: : GOPRT = guarantee obligation persistence recurrence reactivity This =--format= option is also supported by =randltl=, =genltl=, and =ltlgrind=. So for instance if you want to classify the 55 LTL patterns of [[http://patterns.projects.cs.ksu.edu/documentation/patterns/ltl.shtml][Dwyers et al. (FMSP'98)]] using this hierarchy, try:  Alexandre Duret-Lutz committed Apr 17, 2019 116 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 117 118 119 120 121 122 123 124 125 126 127 genltl --dac-patterns --format='%[v]h' | sort | uniq -c #+END_SRC #+RESULTS: : 1 guarantee : 2 obligation : 1 persistence : 2 reactivity : 12 recurrence : 37 safety  Maximilien Colange committed Aug 28, 2017 128 In this output, the most precise class is given for each formula, and  Alexandre Duret-Lutz committed Jan 12, 2017 129 the count of formulas for each subclass is given. We have to remember  Maximilien Colange committed Aug 28, 2017 130 that the recurrence class also includes obligation, safety, and  Alexandre Duret-Lutz committed Jan 12, 2017 131 132 133 134 135 136 137 138 139 guarantee properties. In this list, there are no formulas that belong to the intersection of the /guarantee/ and /safety/ classes (it would have been listed as =guarantee safety=). From this list, only 3 formulas are not recurrence properties (i.e., not recognized by deterministic Büchi automata): one of them is a persistence formula, the other two cannot be classified better than in the /reactivity/ class. Let's pretend we are interested in those three non-recurrence formulas, we can use =ltlfilt -v --recurrence= to  Alexandre Duret-Lutz committed Aug 17, 2017 140 141 remove all recurrence properties from the =genltl --dac-pattern= output:  Alexandre Duret-Lutz committed Jan 12, 2017 142   Alexandre Duret-Lutz committed Apr 17, 2019 143 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 144 145 146 147 148 149 150 151 152 153 genltl --dac-patterns | ltlfilt -v --recurrence --format='%[v]h, %f' #+END_SRC #+RESULTS: : persistence, G!p0 | F(p0 & (!p1 W p2)) : reactivity, G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & X(!p2 U p4)))) U (p2 | G(p1 -> (p3 & XFp4))))) : reactivity, G(p0 -> ((p1 -> (!p2 U (!p2 & p3 & !p4 & X((!p2 & !p4) U p5)))) U (p2 | G(p1 -> (p3 & !p4 & X(!p4 U p5)))))) Similar filtering options exist for other classes. Since these tests  Maximilien Colange committed Aug 28, 2017 154 are automata-based, they work with PSL formulas as well. For instance,  Alexandre Duret-Lutz committed Jan 12, 2017 155 156 157 here is how to generate 10 random recurrence PSL formulas that are not LTL formulas, and that are not obligations:  Alexandre Duret-Lutz committed Apr 17, 2019 158 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 randltl --psl -n -1 a b | ltlfilt -v --ltl | ltlfilt -v --obligation | ltlfilt --recurrence -n10 #+END_SRC #+RESULTS: #+begin_example ((Fb W 0) | (1 U !a)) W ({b[*]}[]-> 0) GF({[*]}<>-> !a) {[*]}[]-> X(b M F!Gb) G!({a[*2]}<>-> (b & F(0 R a))) FX({[*]} -> GFb) G({b[*][:*1]} xor (Fb U Fa)) W b (b R a) & (({1 | [*0]} -> (1 U a)) W 0) G({[*]}[]-> Fa) {[*]}[]-> F(1 U b) 0 R !({!a | a[*]}[]-> GXa) #+end_example Note that the order of the =ltlfilt= filters could be changed provided the =-n10= stays at the end. For instance we could first keep all recurrence before removing obligations and then removing LTL formulas. The order given above actually starts with the easier checks first and keep the most complex tests at the end of the pipeline so they are  Alexandre Duret-Lutz committed Aug 17, 2017 183 184 applied to fewer formulas. Testing whether a formula is an LTL formula is very cheap, testing if a formula is an obligation is harder  Alexandre Duret-Lutz committed Jul 21, 2020 185 (it may involves a translation to automata and a powerset  Alexandre Duret-Lutz committed Aug 17, 2017 186 187 188 189 190 construction), and testing whether a formula is a recurrence is the most costly procedure (it involves a translation as well, plus conversion to deterministic Rabin automata, and an attempt to convert the automaton back to deterministic Büchi). As a rule of thumb, testing classes that are lower in the hierarchy is cheaper.  Alexandre Duret-Lutz committed Jan 12, 2017 191 192 193 194 195 196  Since option =-o= (for specifying output file) also honors =%=-escape sequences, we can use it with =%h= to split a list of formulas in 7 possible files. Here is a generation of 200 random LTL formulas binned into aptly named files:  Alexandre Duret-Lutz committed Apr 17, 2019 197 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 198 199 200 201 202 randltl -n 200 a b -o random-%h.ltl wc -l random-?.ltl #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Apr 17, 2019 203 : 45 random-B.ltl  Alexandre Duret-Lutz committed Jan 12, 2017 204 205 206 207 : 49 random-G.ltl : 12 random-O.ltl : 21 random-P.ltl : 18 random-R.ltl  Alexandre Duret-Lutz committed Apr 17, 2019 208 : 46 random-S.ltl  Alexandre Duret-Lutz committed Jan 12, 2017 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 : 9 random-T.ltl : 200 total #+BEGIN_SRC sh :results silent :exports results rm -f random-?.ltl #+END_SRC #+RESULTS: * Deciding classes membership syntactically LTL formulas can also be classified into related classes which we shall call /syntactic-safety/, /syntactic-guarantee/, etc. See [[https://spot.lrde.epita.fr/tl.pdf][tl.pdf]] for the grammar of each syntactic class. Any LTL-definable property of class C can be defined by an LTL formulas in class syntactic-C, but an LTL formula can describe a property of class C even if that formula is not in class syntactic-C (we just know that some equivalent formula is in class syntactic-C). =ltlfilt= has options like =--syntactic-guarantee=, =--syntactic-persistence=, etc. to match formulas from this classes.  Maximilien Colange committed Aug 28, 2017 230 Here is how to generate 10 random LTL formulas that describe safety  Alexandre Duret-Lutz committed Jan 12, 2017 231 232 properties but that are not in the syntactic-safety class:  Alexandre Duret-Lutz committed Apr 17, 2019 233 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 randltl -n-1 a b | ltlfilt -v --syntactic-safety | ltlfilt --safety -n10 #+END_SRC #+RESULTS: #+begin_example F!(!b <-> FGb) !Fb xor G((b xor (Xa M b)) U b) a W F(a -> b) ((0 R Xa) R a) -> Fa X(Xb & (!Ga R Ga)) (1 U b) | F(Fb W (a <-> FXa)) (a M 1) | (!a W a) (G!a W ((b M 1) -> Fa)) -> !a !a -> ((a xor !GFa) W 0) b M Gb #+end_example Since all those formulas describe safety properties, an exercise would  Maximilien Colange committed Aug 28, 2017 254 be to suggest equivalent formulas that are in the syntactic-safety  Alexandre Duret-Lutz committed Jan 12, 2017 255 256 257 258 fragment. For instance =b M Gb= can be rewritten as just =Gb=, which belongs to this fragment. In this particular case, =ltlfilt --simplify= recognizes this:  Alexandre Duret-Lutz committed Apr 17, 2019 259 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 ltlfilt --simplify -f 'b M Gb' #+END_SRC #+RESULTS: : Gb However in the general case Spot is not able to provide the equivalent formula from the appropriate syntactic class. * What to do with each class? ** Obligation Spot implements algorithms from Löding ([[http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.6718][/Efficient minimization of deterministic weak ω-automata/, IPL 2001]]) and Dax et al. ([[http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.83.2081][/Mechanizing the powerset constructions for restricted classes of ω-automata/, ATVA'07]]) in order to detect obligation properties, and produce minimal weak deterministic automata for them.  Maximilien Colange committed Aug 28, 2017 278 When running =ltl2tgba -D= on a formula that represents an  Alexandre Duret-Lutz committed Jan 12, 2017 279 280 281 282 obligation property, you are guaranteed to obtain a minimal (in the number of states) deterministic weak Büchi automaton that recognizes it. Note that since the /obligation/ class includes the /safety/ and /guarantee/ classes, minimal deterministic automata will also be  Maximilien Colange committed Aug 28, 2017 283 produced for those classes. Dax et al.'s determinization of obligation  Alexandre Duret-Lutz committed Jan 12, 2017 284 properties combined with Löding's minimization renders obsolete  Maximilien Colange committed Aug 28, 2017 285 older algorithms (and tools) that produced minimal deterministic  Alexandre Duret-Lutz committed Jan 12, 2017 286 287 automata but only for the subclasses of /safety/ or /guarantee/.  Alexandre Duret-Lutz committed Aug 17, 2017 288 289 290 291 If =ltl2tgba= is run without =-D= (but still with the default =--high= optimization level), the minimal weak deterministic automaton will only be output if it is smaller than the non-deterministic automaton the translator could produce before determinization and minimization.  Alexandre Duret-Lutz committed Jan 12, 2017 292 293 294  For instance =Fa R b= is an obligation:  Alexandre Duret-Lutz committed Apr 17, 2019 295 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 296 297 298 299 300 301 302 303 304 305 306 ltlfilt -f 'Fa R b' --format='%[v]h' #+END_SRC #+RESULTS: : obligation If we translate it without =-D= we get a 3-state non-deterministic automaton (here we use =autfilt --highlight-nondet= to show where the non-determinism occurs): #+NAME: hier-oblig-1  Alexandre Duret-Lutz committed Apr 17, 2019 307 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 308 309 310 ltl2tgba 'Fa R b' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 311 #+BEGIN_SRC dot :file hier-oblig-1.svg :var txt=hier-oblig-1 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 312 313 314 315 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 316 [[file:hier-oblig-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 317   Alexandre Duret-Lutz committed Jun 25, 2018 318 319 320 321 322 323 324 Note that the default translation used by =ltl2tgba= will turn any syntactic persistence formulas (this includes obligations formulas) into a weak automaton. In a weak automaton, the acceptance condition could be defined in term of SCCs, i.e., the cycles of some SCCs are either all accepting, or all rejecting. As a consequence, it there is no incentive to use transition-based acceptance; instead, state-based acceptance is output by default.  Alexandre Duret-Lutz committed Jan 12, 2017 325 326 327 328 329 330 331 332 333  With =ltl2tgba -D= we get a (minimal) deterministic weak Büchi automaton instead. #+NAME: hier-oblig-2 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -D 'Fa R b' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 334 #+BEGIN_SRC dot :file hier-oblig-2.svg :var txt=hier-oblig-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 335 336 337 338 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 339 [[file:hier-oblig-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 340 341 342 343 344 345 346 347 348 349 350 351  When we called =ltl2tgba=, without the option =-D=, the two automata (non-deterministic and deterministic) were constructed, but the deterministic one was discarded because it was bigger. Using =-D= forces the deterministic automaton to be used regardless of its size. The detection and minimization of obligation properties is also used by =autfilt= when simplifying deterministic automata (they need to be deterministic so that =autfilt= can easily compute their complement). For instance, let us use =ltl2dstar= to construct a Streett automaton  Alexandre Duret-Lutz committed Jun 25, 2018 352 for the obligation property =Ga | XFb=.  Alexandre Duret-Lutz committed Jan 12, 2017 353 354  #+NAME: hier-oblig-3  Alexandre Duret-Lutz committed Apr 17, 2019 355 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jun 25, 2018 356 ltldo 'ltl2dstar --automata=streett' -f 'Ga | XFb' -d  Alexandre Duret-Lutz committed Jan 12, 2017 357 #+END_SRC  Alexandre Duret-Lutz committed Jun 25, 2018 358   Alexandre Duret-Lutz committed Nov 22, 2017 359 #+BEGIN_SRC dot :file hier-oblig-3.svg :var txt=hier-oblig-3 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 360 361 362 363 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 364 [[file:hier-oblig-3.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 365 366 367 368  We can now minimize this automaton with: #+NAME: hier-oblig-4  Alexandre Duret-Lutz committed Apr 17, 2019 369 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jun 25, 2018 370 ltldo 'ltl2dstar --automata=streett' -f 'Ga | XFb' | autfilt -D -C -d  Alexandre Duret-Lutz committed Jan 12, 2017 371 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 372 #+BEGIN_SRC dot :file hier-oblig-4.svg :var txt=hier-oblig-4 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 373 374 375 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 376 [[file:hier-oblig-4.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393  Here we have used option =-C= to keep the automaton complete, so that the comparison with =ltl2dstar= is fair, since =ltl2dstar= always output complete automata. ** Guarantee /Guarantee/ properties can be translated into terminal automata. There is nothing particular in Spot about /guarantee/ properties, they are all handled like /obligations/. Again, using =-D= will always produce (minimal) deterministic Büchi automata, even if they are larger than the non-deterministic version. The output should be a terminal automaton in either case, An example is =a U Xb=:  Alexandre Duret-Lutz committed Apr 17, 2019 394 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 395 396 397 398 399 400 401 402 ltlfilt -f 'a U Xb' --format='%[v]h' #+END_SRC #+RESULTS: : guarantee #+NAME: hier-guarantee-1  Alexandre Duret-Lutz committed Apr 17, 2019 403 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 404 405 ltl2tgba 'a U Xb' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 406 #+BEGIN_SRC dot :file hier-guarantee-1.svg :var txt=hier-guarantee-1 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 407 408 409 410 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 411 [[file:hier-guarantee-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 412 413  #+NAME: hier-guarantee-2  Alexandre Duret-Lutz committed Apr 17, 2019 414 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 415 416 ltl2tgba -D 'a U Xb' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 417 #+BEGIN_SRC dot :file hier-guarantee-2.svg :var txt=hier-guarantee-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 418 419 420 421 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 422 [[file:hier-guarantee-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 423 424  ** Safety  Alexandre Duret-Lutz committed Mar 03, 2017 425 426 427  :PROPERTIES: :CUSTOM_ID: safety :END:  Alexandre Duret-Lutz committed Jan 12, 2017 428 429 430 431 432 433 434  /Safety/ properties also form a subclass of /obligation/ properties, and again there is no code specific to them in the translation. However, the /safety/ class corresponds to what can be represented faithfully by monitors, i.e., automata that accept all their infinite runs.  Maximilien Colange committed Aug 28, 2017 435 For most safety formulas, the acceptance output by =ltl2tgba= will  Alexandre Duret-Lutz committed Jan 12, 2017 436 437 438 439 440 441 442 443 already be =t= (meaning that all runs are accepting). However since the translator does not do anything particular about safety formulas, it is possible to find some pathological formulas for which the translator outputs a non-deterministic Büchi automaton where not all run are accepting. Here is an example:  Alexandre Duret-Lutz committed Apr 17, 2019 444 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 445 446 447 448 449 450 451 452 ltlfilt -f '(a W Gb) M b' --format='%[v]h' #+END_SRC #+RESULTS: : safety #+NAME: hier-safety-1  Alexandre Duret-Lutz committed Apr 17, 2019 453 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 454 455 ltl2tgba '(a W Gb) M b' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 456 #+BEGIN_SRC dot :file hier-safety-1.svg :var txt=hier-safety-1 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 457 458 459 460 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 461 [[file:hier-safety-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 462 463 464 465 466  Actually, marking all states of this automaton as accepting would not be wrong, the translator simply does not know it. Using =-D= will fix that: it then produces a deterministic automaton  Alexandre Duret-Lutz committed Aug 17, 2017 467 that is guaranteed to be minimal, and where all runs are accepting.  Alexandre Duret-Lutz committed Jan 12, 2017 468 469  #+NAME: hier-safety-2  Alexandre Duret-Lutz committed Apr 17, 2019 470 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 471 472 ltl2tgba -D '(a W Gb) M b' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 473 #+BEGIN_SRC dot :file hier-safety-2.svg :var txt=hier-safety-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 474 475 476 477 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 478 [[file:hier-safety-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 479 480   Alexandre Duret-Lutz committed Aug 17, 2017 481 482 483 484 If you are working with safety formula, and know you want to work with monitors, you can use the =-M= option of =ltl2tgba=. In this case this will output the same automaton, but using the universal acceptance (i.e. =t=). You can interpret this output as a monitor  Maximilien Colange committed Aug 28, 2017 485 (i.e., a finite automaton that accepts all prefixes that can be  Alexandre Duret-Lutz committed Aug 17, 2017 486 extended into valid ω-words).  Alexandre Duret-Lutz committed Jan 12, 2017 487 488  #+NAME: hier-safety-1m  Alexandre Duret-Lutz committed Apr 17, 2019 489 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 490 491 ltl2tgba -M '(a W Gb) M b' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 492 #+BEGIN_SRC dot :file hier-safety-1m.svg :var txt=hier-safety-1m :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 493 494 495 496  $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 497 [[file:hier-safety-1m.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 498 499  #+NAME: hier-safety-2m  Alexandre Duret-Lutz committed Apr 17, 2019 500 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 501 502 ltl2tgba -M -D '(a W Gb) M b' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 503 #+BEGIN_SRC dot :file hier-safety-2m.svg :var txt=hier-safety-2m :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 504 505 506 507 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 508 [[file:hier-safety-2m.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 509 510 511 512 513 514 515 516 517 518 519 520  Note that the =-M= option can be used with formulas that are not safety properties. In this case, the output monitor will recognize a language larger than that of the property. ** Recurrence /Recurrence/ properties can be represented by deterministic Büchi automata. For the subclass of /obligation/ properties, using =-D= is a sure way  Alexandre Duret-Lutz committed Jul 21, 2020 521 to obtain a deterministic automaton (and even a minimal one), but for  Alexandre Duret-Lutz committed Jan 12, 2017 522 the /recurrence/ properties that are not /obligations/ the translator  Alexandre Duret-Lutz committed Jun 12, 2019 523 does not make /too much/ effort to produce deterministic automata,  Alexandre Duret-Lutz committed Aug 17, 2017 524 even with =-D= (this might change in the future).  Alexandre Duret-Lutz committed Jan 12, 2017 525   Alexandre Duret-Lutz committed Aug 17, 2017 526 527 528 529 All properties that are not in the /persistence/ class (this includes the /recurrence/ properties that are not /obligations/) can benefit from transition-based acceptance. In other words using transition-based acceptance will often produce shorter automata.  Alexandre Duret-Lutz committed Jan 12, 2017 530 531 532 533  The typical example is =GFa=, which can be translated into a 1-state transition-based Büchi automaton:  Alexandre Duret-Lutz committed Apr 17, 2019 534 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 535 536 537 538 539 540 541 ltlfilt -f 'GFa' --format='%[v]h' #+END_SRC #+RESULTS: : recurrence #+NAME: hier-recurrence-1  Alexandre Duret-Lutz committed Apr 17, 2019 542 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 543 544 ltl2tgba 'GFa' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 545 #+BEGIN_SRC dot :file hier-recurrence-1.svg :var txt=hier-recurrence-1 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 546 547 548 549 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 550 [[file:hier-recurrence-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 551 552 553 554  Using state-based acceptance, at least two states are required. For instance: #+NAME: hier-recurrence-2  Alexandre Duret-Lutz committed Apr 17, 2019 555 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 556 557 ltl2tgba -S 'GFa' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 558 #+BEGIN_SRC dot :file hier-recurrence-2.svg :var txt=hier-recurrence-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 559 560 561 562 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 563 [[file:hier-recurrence-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 564 565   Maximilien Colange committed Aug 28, 2017 566 Here is an example of a formula for which =ltl2tgba= does not produce a  Alexandre Duret-Lutz committed Jan 12, 2017 567 568 deterministic automaton, even with =-D=.  Alexandre Duret-Lutz committed Apr 17, 2019 569 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 570 571 572 573 574 575 576 ltlfilt -f 'G(Gb | Fa)' --format='%[v]h' #+END_SRC #+RESULTS: : recurrence #+NAME: hier-recurrence-3  Alexandre Duret-Lutz committed Apr 17, 2019 577 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 578 579 ltl2tgba -D 'G(Gb | Fa)' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 580 #+BEGIN_SRC dot :file hier-recurrence-3.svg :var txt=hier-recurrence-3 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 581 582 583 584 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 585 [[file:hier-recurrence-3.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 586 587  One way to obtain a deterministic Büchi automaton (it has to exist, since this is  Alexandre Duret-Lutz committed Jun 12, 2019 588 589 590 591 592 593 a /recurrence/ property), is to request a deterministic automaton with parity acceptance using =-P=. The number of color output with =-P= is always reduced to the minimal number possible, so for a /recurrence/ property the output automaton can only have one of three possible acceptance: =Inf(0)=, =t=, or =f=. #+NAME: hier-recurrence-4  Alexandre Duret-Lutz committed Apr 17, 2019 594 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jun 12, 2019 595 ltl2tgba -P -D 'G(Gb | Fa)' -d  Alexandre Duret-Lutz committed Aug 17, 2017 596 #+END_SRC  Alexandre Duret-Lutz committed Jun 12, 2019 597 #+BEGIN_SRC dot :file hier-recurrence-4.svg :var txt=hier-recurrence-4 :exports results  Alexandre Duret-Lutz committed Aug 17, 2017 598 599 $txt #+END_SRC  Alexandre Duret-Lutz committed Jun 12, 2019 600 601 602 603 604 605 606 #+RESULTS: [[file:hier-recurrence-4.svg]] Note that if the acceptance is =t=, the property is a monitor, and if its =f=, the property is =false=. In any way, if you would like to obtain a DBA for any recurrent property, a sure way to avoid these difference is to pipe the result through =autfilt -B=  Alexandre Duret-Lutz committed Aug 17, 2017 607   Alexandre Duret-Lutz committed Jun 12, 2019 608 609 610 611 612 613 614 #+NAME: hier-recurrence-5 #+BEGIN_SRC sh :exports code ltl2tgba -P -D 'G(Gb | Fa)' | autfilt -B -d #+END_SRC #+BEGIN_SRC dot :file hier-recurrence-5.svg :var txt=hier-recurrence-5 :exports results $txt #+END_SRC  Alexandre Duret-Lutz committed Aug 17, 2017 615 #+RESULTS:  Alexandre Duret-Lutz committed Jun 12, 2019 616 [[file:hier-recurrence-5.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 617   Alexandre Duret-Lutz committed Jun 12, 2019 618 619 620 621  It is likely that =ltl2tgba -B -D= will implement these steps in the future, but so originally =-D= was only expressing a preference not a requirement.  Alexandre Duret-Lutz committed Jan 12, 2017 622 623 624 625 626 627 628 629  ** Persistence Since /persistence/ properties are outside of the /recurrence/ class, they cannot be represented by deterministic Büchi automata. The typical persistence formula is =FGa=, and using =-D= on this is hopeless. #+NAME: hier-persistence-1  Alexandre Duret-Lutz committed Apr 17, 2019 630 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 631 ltl2tgba -D FGa -d  Alexandre Duret-Lutz committed Jan 12, 2017 632 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 633 #+BEGIN_SRC dot :file hier-persistence-1.svg :var txt=hier-persistence-1 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 634 635 636 637 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 638 [[file:hier-persistence-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 639 640 641 642 643 644 645 646 647  However since the *negation* of =FGa= is a /recurrence/, this negation can be represented by a deterministic Büchi automaton, which means that =FGa= could be represented by a deterministic co-Büchi automaton. =ltl2tgba= does not generate co-Büchi acceptance, but we can do the complementation ourselves: #+NAME: hier-persistence-2  Alexandre Duret-Lutz committed Apr 17, 2019 648 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Sep 23, 2019 649 ltl2tgba --negate -D FGa | autfilt --complement -d  Alexandre Duret-Lutz committed Jan 12, 2017 650 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 651 #+BEGIN_SRC dot :file hier-persistence-2.svg :var txt=hier-persistence-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 652 653 654 655 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 656 [[file:hier-persistence-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 657 658 659  Note that in this example, we know that =GFa= is trivial enough that =ltl2tgba -D GFa= will generate a deterministic automaton. In the  Alexandre Duret-Lutz committed Jun 12, 2019 660 661 662 general case we might have to determinize the automaton using =-P -D= as we did in the previous section. For persistence properties, =-P -D= should return an automaton whose acceptance is one of =Fin(0)=, =t=, or =f=.  Alexandre Duret-Lutz committed Jan 12, 2017 663   Alexandre Duret-Lutz committed Jun 25, 2018 664 665 666 667 668 /Persistence/ properties can be represented by weak Büchi automata. The translator is aware of that, so when it detects that the input formula is a syntactic-persistence, it simplifies its translation slightly to ensure that the output will use at most one acceptance set. (It is possible to define a persistence properties using an LTL  Alexandre Duret-Lutz committed Jul 21, 2020 669 formula that is not a syntactic-persistence, in that case this  Alexandre Duret-Lutz committed Jun 25, 2018 670 optimization is simply not applied.)  Alexandre Duret-Lutz committed Jan 12, 2017 671 672 673 674  If the input is a weak property that is not syntactically weak, the output will not necessarily be weak. One costly way to obtain a weak automaton for a formula$\varphi$would be to first compute a  Alexandre Duret-Lutz committed Jun 12, 2019 675 676 deterministic co-Büchi automaton$\varphi$then transform that into a Büchi automaton.  Alexandre Duret-Lutz committed Jan 12, 2017 677   Alexandre Duret-Lutz committed Jun 25, 2018 678 679 Let's do that on the persistence formula =F(G!a | G(b U a))=, just for the fun of it.  Alexandre Duret-Lutz committed Jan 12, 2017 680   Alexandre Duret-Lutz committed Apr 17, 2019 681 #+BEGIN_SRC sh  Alexandre Duret-Lutz committed Jan 12, 2017 682 683 684 685 686 687 688 689 ltlfilt -f 'F(G!a | G(b U a))' --format='%[v]h' #+END_SRC #+RESULTS: : persistence Unfortunately the default output of the translation is not weak: #+NAME: hier-persistence-3  Alexandre Duret-Lutz committed Apr 17, 2019 690 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jan 12, 2017 691 692 ltl2tgba 'F(G!a | G(b U a))' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 693 #+BEGIN_SRC dot :file hier-persistence-3.svg :var txt=hier-persistence-3 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 694 695 696 697 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 698 [[file:hier-persistence-3.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 699   Alexandre Duret-Lutz committed Jun 12, 2019 700 So let's determinize using parity acceptance:  Alexandre Duret-Lutz committed Jan 12, 2017 701 702  #+NAME: hier-persistence-4  Alexandre Duret-Lutz committed Apr 17, 2019 703 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jun 12, 2019 704 ltl2tgba -P -D 'F(G!a | G(b U a))' -d  Alexandre Duret-Lutz committed Jan 12, 2017 705 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 706 #+BEGIN_SRC dot :file hier-persistence-4.svg :var txt=hier-persistence-4 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 707 708 709 710 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 711 [[file:hier-persistence-4.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 712   Alexandre Duret-Lutz committed Jun 12, 2019 713 And finally we convert the result back to Büchi with =autfilt -B=.  Alexandre Duret-Lutz committed Jan 12, 2017 714 715  #+NAME: hier-persistence-7  Alexandre Duret-Lutz committed Apr 17, 2019 716 #+BEGIN_SRC sh :exports code  Alexandre Duret-Lutz committed Jun 12, 2019 717 ltl2tgba -P -D 'F(G!a | G(b U a))' | autfilt -B --highlight-nondet --small -d  Alexandre Duret-Lutz committed Jan 12, 2017 718 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 719 #+BEGIN_SRC dot :file hier-persistence-7.svg :var txt=hier-persistence-7 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 720 721 722 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 723 [[file:hier-persistence-7.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 724   Alexandre Duret-Lutz committed Jun 12, 2019 725 That is indeed, a weak non-deterministic automaton.  Alexandre Duret-Lutz committed Jul 21, 2020 726 727 728 729 730 731 732  # LocalWords: utf Pnueli html args PODC SCC subexpressions mathsf # LocalWords: SRC ltlfilt vw GOPRT randltl genltl ltlgrind Dwyers # LocalWords: et al FMSP dac uniq XFp psl Fb GF Gb FX GFb GXa wc tl # LocalWords: powerset pdf FGb Xa Xb FXa GFa Löding IPL Dax ATVA # LocalWords: tgba Löding's nondet hier oblig svg txt SCCs dstar # LocalWords: XFb ltldo streett DBA FGa varphi