hierarchy.org 27.7 KB
 Alexandre Duret-Lutz committed Jan 12, 2017 1 2 3 4 5 6 7 # -*- coding: utf-8 -*- #+TITLE: Exploring the temporal hierarchy of Manna & Pnueli #+DESCRIPTION: Spot command-line tools for exploring the temporal hierarchy of Manna & Pnueli #+SETUPFILE: setup.org #+HTML_LINK_UP: tools.html /A hierarchy of temporal properties/ was defined by Manna & Pnueli in  Alexandre Duret-Lutz committed Aug 17, 2017 8 their [[ftp://www-cs.stanford.edu/cs/theory/amir/hierarchy.ps][PODC'90 paper]].  Alexandre Duret-Lutz committed Jan 12, 2017 9 10 11 12 13 14 15 16 17  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 18 19 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 20   Alexandre Duret-Lutz committed Nov 22, 2017 21 [[file:hierarchy.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 22 23 24 25  Forget about the LTL properties and about the red letters displayed in this picture for a moment.  Alexandre Duret-Lutz committed Aug 17, 2017 26 27 28 - 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 29   Alexandre Duret-Lutz committed Aug 17, 2017 30 31 - The /recurrence/ subclass contains all properties that can be recognized by a deterministic Büchi automaton.  Alexandre Duret-Lutz committed Jan 12, 2017 32   Alexandre Duret-Lutz committed Aug 17, 2017 33 - The dual class, /persistence/ properties, are those that can be  Maximilien Colange committed Aug 28, 2017 34  recognized by a weak Büchi automaton (i.e., in each SCC either all  Alexandre Duret-Lutz committed Aug 17, 2017 35  states are accepting, or all states are rejecting).  Alexandre Duret-Lutz committed Jan 12, 2017 36   Alexandre Duret-Lutz committed Aug 17, 2017 37 38 39 - 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 40   Alexandre Duret-Lutz committed Aug 17, 2017 41 42 43 - /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 44   Alexandre Duret-Lutz committed Aug 17, 2017 45 - /Safety/ properties are the dual of /Guarantee/ properties: they can  Maximilien Colange committed Aug 28, 2017 46  be recognized by ω-automata that accept all their runs (i.e., the  Alexandre Duret-Lutz committed Aug 17, 2017 47  acceptance condition is "true"). Note that since these automata are  Maximilien Colange committed Aug 28, 2017 48  not necessary complete, it is still possible for some words not to  Alexandre Duret-Lutz committed Aug 17, 2017 49 50 51 52  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 53   Maximilien Colange committed Aug 28, 2017 54 - Finally, at the very bottom is an unnamed class that contains  Alexandre Duret-Lutz committed Aug 17, 2017 55 56 57  /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 58 59 60  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 61 that (1) this hierarchy applies to all omega-regular properties, not  Alexandre Duret-Lutz committed Jan 12, 2017 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 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/ and /guarentee/ properties, while /reactivity/ properties are Boolean 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. #+BEGIN_SRC sh :results verbatim :exports both 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=: #+BEGIN_SRC sh :results verbatim :exports both 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=: #+BEGIN_SRC sh :results verbatim :exports both 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: #+BEGIN_SRC sh :results verbatim :exports both 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 127 In this output, the most precise class is given for each formula, and  Alexandre Duret-Lutz committed Jan 12, 2017 128 the count of formulas for each subclass is given. We have to remember  Maximilien Colange committed Aug 28, 2017 129 that the recurrence class also includes obligation, safety, and  Alexandre Duret-Lutz committed Jan 12, 2017 130 131 132 133 134 135 136 137 138 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 139 140 remove all recurrence properties from the =genltl --dac-pattern= output:  Alexandre Duret-Lutz committed Jan 12, 2017 141 142 143 144 145 146 147 148 149 150 151 152  #+BEGIN_SRC sh :results verbatim :exports both 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 153 are automata-based, they work with PSL formulas as well. For instance,  Alexandre Duret-Lutz committed Jan 12, 2017 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 here is how to generate 10 random recurrence PSL formulas that are not LTL formulas, and that are not obligations: #+BEGIN_SRC sh :results verbatim :exports both 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 182 183 184 185 186 187 188 189 applied to fewer formulas. Testing whether a formula is an LTL formula is very cheap, testing if a formula is an obligation is harder (it may involves a translation to automata and a poweset 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 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228  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: #+BEGIN_SRC sh :results verbatim :exports both randltl -n 200 a b -o random-%h.ltl wc -l random-?.ltl #+END_SRC #+RESULTS: : 40 random-B.ltl : 49 random-G.ltl : 12 random-O.ltl : 21 random-P.ltl : 18 random-R.ltl : 51 random-S.ltl : 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 229 Here is how to generate 10 random LTL formulas that describe safety  Alexandre Duret-Lutz committed Jan 12, 2017 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 properties but that are not in the syntactic-safety class: #+BEGIN_SRC sh :results verbatim :exports both 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 253 be to suggest equivalent formulas that are in the syntactic-safety  Alexandre Duret-Lutz committed Jan 12, 2017 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 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: #+BEGIN_SRC sh :results verbatim :exports both 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 277 When running =ltl2tgba -D= on a formula that represents an  Alexandre Duret-Lutz committed Jan 12, 2017 278 279 280 281 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 282 produced for those classes. Dax et al.'s determinization of obligation  Alexandre Duret-Lutz committed Jan 12, 2017 283 properties combined with Löding's minimization renders obsolete  Maximilien Colange committed Aug 28, 2017 284 older algorithms (and tools) that produced minimal deterministic  Alexandre Duret-Lutz committed Jan 12, 2017 285 286 automata but only for the subclasses of /safety/ or /guarantee/.  Alexandre Duret-Lutz committed Aug 17, 2017 287 288 289 290 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 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309  For instance =Fa R b= is an obligation: #+BEGIN_SRC sh :results verbatim :exports both 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 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba 'Fa R b' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 310 #+BEGIN_SRC dot :file hier-oblig-1.svg :var txt=hier-oblig-1 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 311 312 313 314 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 315 [[file:hier-oblig-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 316 317 318 319 320 321 322 323 324 325 326  Note that the above automaton uses transition-based acceptance, but since it is an obligation, using transition-based acceptance will not improve anything, so we might as well require a Büchi automaton with =-B= or just state-based acceptance with =-S=: #+NAME: hier-oblig-1b #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -B 'Fa R b' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 327 #+BEGIN_SRC dot :file hier-oblig-1b.svg :var txt=hier-oblig-1b :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 328 329 330 331 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 332 [[file:hier-oblig-1b.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 333 334 335 336 337 338 339 340 341 342  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 343 #+BEGIN_SRC dot :file hier-oblig-2.svg :var txt=hier-oblig-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 344 345 346 347 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 348 [[file:hier-oblig-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364  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 for the obligation property =a <-> GXa=: #+NAME: hier-oblig-3 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 365 ltldo 'ltl2dstar --automata=streett' -f 'a <-> GXa' -d  Alexandre Duret-Lutz committed Jan 12, 2017 366 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 367 #+BEGIN_SRC dot :file hier-oblig-3.svg :var txt=hier-oblig-3 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 368 369 370 371 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 372 [[file:hier-oblig-3.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 373 374 375 376 377 378 379  We can now minimize this automaton with: #+NAME: hier-oblig-4 #+BEGIN_SRC sh :results verbatim :exports code ltldo 'ltl2dstar --automata=streett' -f 'a <-> GXa' | autfilt -D -C -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 380 #+BEGIN_SRC dot :file hier-oblig-4.svg :var txt=hier-oblig-4 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 381 382 383 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 384 [[file:hier-oblig-4.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413  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=: #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f 'a U Xb' --format='%[v]h' #+END_SRC #+RESULTS: : guarantee #+NAME: hier-guarantee-1 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba 'a U Xb' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 414 #+BEGIN_SRC dot :file hier-guarantee-1.svg :var txt=hier-guarantee-1 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 415 416 417 418 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 419 [[file:hier-guarantee-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 420 421 422 423 424  #+NAME: hier-guarantee-2 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -D 'a U Xb' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 425 #+BEGIN_SRC dot :file hier-guarantee-2.svg :var txt=hier-guarantee-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 426 427 428 429 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 430 [[file:hier-guarantee-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 431 432  ** Safety  Alexandre Duret-Lutz committed Mar 03, 2017 433 434 435  :PROPERTIES: :CUSTOM_ID: safety :END:  Alexandre Duret-Lutz committed Jan 12, 2017 436 437 438 439 440 441 442  /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 443 For most safety formulas, the acceptance output by =ltl2tgba= will  Alexandre Duret-Lutz committed Jan 12, 2017 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 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: #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f '(a W Gb) M b' --format='%[v]h' #+END_SRC #+RESULTS: : safety #+NAME: hier-safety-1 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba '(a W Gb) M b' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 464 #+BEGIN_SRC dot :file hier-safety-1.svg :var txt=hier-safety-1 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 465 466 467 468 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 469 [[file:hier-safety-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 470 471 472 473 474  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 475 that is guaranteed to be minimal, and where all runs are accepting.  Alexandre Duret-Lutz committed Jan 12, 2017 476 477 478 479 480  #+NAME: hier-safety-2 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -D '(a W Gb) M b' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 481 #+BEGIN_SRC dot :file hier-safety-2.svg :var txt=hier-safety-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 482 483 484 485 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 486 [[file:hier-safety-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 487 488   Alexandre Duret-Lutz committed Aug 17, 2017 489 490 491 492 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 493 (i.e., a finite automaton that accepts all prefixes that can be  Alexandre Duret-Lutz committed Aug 17, 2017 494 extended into valid ω-words).  Alexandre Duret-Lutz committed Jan 12, 2017 495 496 497 498 499  #+NAME: hier-safety-1m #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -M '(a W Gb) M b' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 500 #+BEGIN_SRC dot :file hier-safety-1m.svg :var txt=hier-safety-1m :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 501 502 503 504 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 505 [[file:hier-safety-1m.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 506 507 508 509 510  #+NAME: hier-safety-2m #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -M -D '(a W Gb) M b' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 511 #+BEGIN_SRC dot :file hier-safety-2m.svg :var txt=hier-safety-2m :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 512 513 514 515 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 516 [[file:hier-safety-2m.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531  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 to obain a deterministic automaton (and even a minimal one), but for the /recurrence/ properties that are not /obligations/ the translator does not make any special effort to produce deterministic automata,  Alexandre Duret-Lutz committed Aug 17, 2017 532 even with =-D= (this might change in the future).  Alexandre Duret-Lutz committed Jan 12, 2017 533   Alexandre Duret-Lutz committed Aug 17, 2017 534 535 536 537 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 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552  The typical example is =GFa=, which can be translated into a 1-state transition-based Büchi automaton: #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f 'GFa' --format='%[v]h' #+END_SRC #+RESULTS: : recurrence #+NAME: hier-recurrence-1 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba 'GFa' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 553 #+BEGIN_SRC dot :file hier-recurrence-1.svg :var txt=hier-recurrence-1 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 554 555 556 557 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 558 [[file:hier-recurrence-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 559 560 561 562 563 564 565  Using state-based acceptance, at least two states are required. For instance: #+NAME: hier-recurrence-2 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -S 'GFa' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 566 #+BEGIN_SRC dot :file hier-recurrence-2.svg :var txt=hier-recurrence-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 567 568 569 570 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 571 [[file:hier-recurrence-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 572 573   Maximilien Colange committed Aug 28, 2017 574 Here is an example of a formula for which =ltl2tgba= does not produce a  Alexandre Duret-Lutz committed Jan 12, 2017 575 576 577 578 579 580 581 582 583 584 585 586 587 deterministic automaton, even with =-D=. #+BEGIN_SRC sh :results verbatim :exports both ltlfilt -f 'G(Gb | Fa)' --format='%[v]h' #+END_SRC #+RESULTS: : recurrence #+NAME: hier-recurrence-3 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -D 'G(Gb | Fa)' | autfilt --highlight-nondet -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 588 #+BEGIN_SRC dot :file hier-recurrence-3.svg :var txt=hier-recurrence-3 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 589 590 591 592 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 593 [[file:hier-recurrence-3.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 594 595 596 597  One way to obtain a deterministic Büchi automaton (it has to exist, since this is a /recurrence/ property), is to chain a few algorithms implemented in Spot:  Alexandre Duret-Lutz committed Aug 17, 2017 598  1. Determinize the non-deterministic automaton to obtain a  Alexandre Duret-Lutz committed Jan 12, 2017 599 600 601 602 603 604  deterministic automaton with parity acceptance: this is done by using =ltl2tgba -G -D=, with option =-G= indicating that any acceptance condition may be used. #+NAME: hier-recurrence-4 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 605  ltl2tgba -G -D 'G(Gb | Fa)' -d  Alexandre Duret-Lutz committed Jan 12, 2017 606  #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 607  #+BEGIN_SRC dot :file hier-recurrence-4.svg :var txt=hier-recurrence-4 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 608 609 610  $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 611  [[file:hier-recurrence-4.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 612   Alexandre Duret-Lutz committed Aug 17, 2017 613  2. Transform the parity acceptance into Rabin acceptance: this is  Alexandre Duret-Lutz committed Jan 12, 2017 614 615 616 617 618 619 620  done with =autfilt --generalized-rabin=. Because of the type of parity acceptance used, the result will actually be Rabin and not generalized Rabin. #+NAME: hier-recurrence-5 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -G -D 'G(Gb | Fa)' |  Alexandre Duret-Lutz committed Mar 10, 2018 621  autfilt --generalized-rabin -d  Alexandre Duret-Lutz committed Jan 12, 2017 622  #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 623  #+BEGIN_SRC dot :file hier-recurrence-5.svg :var txt=hier-recurrence-5 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 624 625 626 627 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 628  [[file:hier-recurrence-5.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 629 630 631  (The only change here is in the acceptance condition.)  Alexandre Duret-Lutz committed Aug 17, 2017 632  3. In step 4 we are going to convert the automaton to state-based  Maximilien Colange committed Aug 28, 2017 633 634  Büchi, and this sometimes works better if the input Rabin automaton also uses state-based acceptance. So let us add =-S= to the  Alexandre Duret-Lutz committed Aug 17, 2017 635  previous command:  Alexandre Duret-Lutz committed Jan 12, 2017 636 637 638 639  #+NAME: hier-recurrence-6 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -G -D 'G(Gb | Fa)' |  Alexandre Duret-Lutz committed Mar 10, 2018 640  autfilt -S --generalized-rabin -d  Alexandre Duret-Lutz committed Jan 12, 2017 641  #+END_SRC  Alexandre Duret-Lutz committed Aug 17, 2017 642   Alexandre Duret-Lutz committed Nov 22, 2017 643  #+BEGIN_SRC dot :file hier-recurrence-6.svg :var txt=hier-recurrence-6 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 644 645 646 647  $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 648  [[file:hier-recurrence-6.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 649   Alexandre Duret-Lutz committed Jun 30, 2017 650  4. Finally, convert the resulting automaton to BA, using =autfilt  Alexandre Duret-Lutz committed Aug 17, 2017 651 652 653 654 655 656 657 658  -B=. Spot can convert automata with any acceptance condition to BA, but when the input is a deterministic Rabin automaton, it uses a dedicated algorithm that preserves determinism whenever possible (and we know it is possible, because we are working on a recurrence formula). Adding =-D= here to suggest that we are trying to obtain a deterministic automaton does not hurt, as it will enable simplifications as a side-effect (without =-D= we simply get a larger deterministic automaton).  Alexandre Duret-Lutz committed Jan 12, 2017 659 660 661 662 663  #+NAME: hier-recurrence-7 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -G -D 'G(Gb | Fa)' | autfilt -S --generalized-rabin |  Alexandre Duret-Lutz committed Mar 10, 2018 664  autfilt -B -D -d  Alexandre Duret-Lutz committed Jan 12, 2017 665  #+END_SRC  Alexandre Duret-Lutz committed Aug 17, 2017 666   Alexandre Duret-Lutz committed Nov 22, 2017 667  #+BEGIN_SRC dot :file hier-recurrence-7.svg :var txt=hier-recurrence-7 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 668 669 670 671 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 672  [[file:hier-recurrence-7.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 673 674  Here we are lucky that the deterministic Büchi automaton is even  Alexandre Duret-Lutz committed Aug 17, 2017 675 676 677 678 679 680 681 682 smaller than the original non-deterministic version. As said earlier, passing =-S= to the first =autfilt= was optional, but in this case it helps producing a smaller automaton. Here is what we get without it: #+NAME: hier-recurrence-8 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba -G -D 'G(Gb | Fa)' | autfilt --generalized-rabin |  Alexandre Duret-Lutz committed Mar 10, 2018 683  autfilt -B -D -d  Alexandre Duret-Lutz committed Aug 17, 2017 684 685 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 686 #+BEGIN_SRC dot :file hier-recurrence-8.svg :var txt=hier-recurrence-8 :exports results  Alexandre Duret-Lutz committed Aug 17, 2017 687 688 689 690 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 691 [[file:hier-recurrence-8.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 692 693  It is likely that =ltl2tgba= will implement all this processing chain  Alexandre Duret-Lutz committed Aug 17, 2017 694 in the future.  Alexandre Duret-Lutz committed Jan 12, 2017 695 696 697 698 699 700 701 702 703  ** 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 #+BEGIN_SRC sh :results verbatim :exports code  Alexandre Duret-Lutz committed Mar 10, 2018 704 ltl2tgba -D FGa -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-1.svg :var txt=hier-persistence-1 :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-1.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 712 713 714 715 716 717 718 719 720 721 722 723  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 #+BEGIN_SRC sh :results verbatim :exports code ltlfilt --negate -f FGa | ltl2tgba -D |  Alexandre Duret-Lutz committed Mar 10, 2018 724  autfilt --complement -d  Alexandre Duret-Lutz committed Jan 12, 2017 725 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 726 #+BEGIN_SRC dot :file hier-persistence-2.svg :var txt=hier-persistence-2 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 727 728 729 730 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 731 [[file:hier-persistence-2.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767  Note that in this example, we know that =GFa= is trivial enough that =ltl2tgba -D GFa= will generate a deterministic automaton. In the general case we might have to determinize the automaton as we did in the previous section (we will do it again below). /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 formula that is not a syntactic-persistance, this optimization is simply not applied.) 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 deterministic Büchi automaton of the recurrence$\lnot\varphi$then complement the acceptance of the resulting automaton, yielding a deterministic co-Büchi automaton, and then transform that into a Büchi automaton. Let's do that on the persistence formula =F(G!a | G(b U a))= #+BEGIN_SRC sh :results verbatim :exports both 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 #+BEGIN_SRC sh :results verbatim :exports code ltl2tgba 'F(G!a | G(b U a))' -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 768 #+BEGIN_SRC dot :file hier-persistence-3.svg :var txt=hier-persistence-3 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 769 770 771 772 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 773 [[file:hier-persistence-3.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 774 775 776 777 778 779 780 781 782  Furthermore it appears that =ltl2tgba= does generate a deterministic Büchi automaton for the complement, instead we get a non-deterministic generalized Büchi automaton: #+NAME: hier-persistence-4 #+BEGIN_SRC sh :results verbatim :exports code ltlfilt --negate -f 'F(G!a | G(b U a))' | ltl2tgba -D |  Alexandre Duret-Lutz committed Mar 10, 2018 783  autfilt --highlight-nondet=5 -d  Alexandre Duret-Lutz committed Jan 12, 2017 784 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 785 #+BEGIN_SRC dot :file hier-persistence-4.svg :var txt=hier-persistence-4 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 786 787 788 789 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 790 [[file:hier-persistence-4.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 791   Alexandre Duret-Lutz committed Aug 17, 2017 792 793 So let us use the same tricks as in the previous section, determinizing this automaton into a Rabin automaton, and then back to  Alexandre Duret-Lutz committed Jan 12, 2017 794 795 796 797 798 799 deterministic Büchi: #+NAME: hier-persistence-5 #+BEGIN_SRC sh :results verbatim :exports code ltlfilt --negate -f 'F(G!a | G(b U a))' | ltl2tgba -G -D |  Alexandre Duret-Lutz committed Aug 17, 2017 800  autfilt --generalized-rabin |  Alexandre Duret-Lutz committed Mar 10, 2018 801  autfilt --tgba -D -d  Alexandre Duret-Lutz committed Jan 12, 2017 802 #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 803 #+BEGIN_SRC dot :file hier-persistence-5.svg :var txt=hier-persistence-5 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 804 805 806 807 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 808 [[file:hier-persistence-5.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 809 810 811 812 813 814 815 816  This is a deterministic Büchi automaton for the negation of our formula. Now we can complement it to obtain a deterministic co-Büchi automaton for =F(G!a | G(b U a))=: #+NAME: hier-persistence-6 #+BEGIN_SRC sh :results verbatim :exports code ltlfilt --negate -f 'F(G!a | G(b U a))' | ltl2tgba -G -D |  Alexandre Duret-Lutz committed Aug 17, 2017 817  autfilt --generalized-rabin |  Alexandre Duret-Lutz committed Jan 12, 2017 818  autfilt --tgba -D |  Alexandre Duret-Lutz committed Mar 10, 2018 819  autfilt --complement -d  Alexandre Duret-Lutz committed Jan 12, 2017 820 #+END_SRC  Alexandre Duret-Lutz committed Mar 10, 2018 821   Alexandre Duret-Lutz committed Nov 22, 2017 822 #+BEGIN_SRC dot :file hier-persistence-6.svg :var txt=hier-persistence-6 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 823 824 825 826 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 827 [[file:hier-persistence-6.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 828 829 830 831 832 833 834  And finally we convert the result back to Büchi: #+NAME: hier-persistence-7 #+BEGIN_SRC sh :results verbatim :exports code ltlfilt --negate -f 'F(G!a | G(b U a))' | ltl2tgba -G -D |  Alexandre Duret-Lutz committed Aug 17, 2017 835  autfilt --generalized-rabin |  Alexandre Duret-Lutz committed Jan 12, 2017 836 837 838 839  autfilt --tgba -D | autfilt --complement -B -d #+END_SRC  Alexandre Duret-Lutz committed Nov 22, 2017 840 #+BEGIN_SRC dot :file hier-persistence-7.svg :var txt=hier-persistence-7 :exports results  Alexandre Duret-Lutz committed Jan 12, 2017 841 842 843 $txt #+END_SRC #+RESULTS:  Alexandre Duret-Lutz committed Nov 22, 2017 844 [[file:hier-persistence-7.svg]]  Alexandre Duret-Lutz committed Jan 12, 2017 845 846  That is indeed, a weak automaton.