equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{CTL}% |
3 \def\isabellecontext{CTL}% |
|
4 \isamarkupfalse% |
4 % |
5 % |
5 \isadelimtheory |
6 \isadelimtheory |
6 % |
7 % |
7 \endisadelimtheory |
8 \endisadelimtheory |
8 % |
9 % |
9 \isatagtheory |
10 \isatagtheory |
10 \isamarkupfalse% |
|
11 % |
11 % |
12 \endisatagtheory |
12 \endisatagtheory |
13 {\isafoldtheory}% |
13 {\isafoldtheory}% |
14 % |
14 % |
15 \isadelimtheory |
15 \isadelimtheory |
27 Let us be adventurous and introduce a more expressive temporal operator. |
27 Let us be adventurous and introduce a more expressive temporal operator. |
28 We extend the datatype |
28 We extend the datatype |
29 \isa{formula} by a new constructor% |
29 \isa{formula} by a new constructor% |
30 \end{isamarkuptext}% |
30 \end{isamarkuptext}% |
31 \isamarkuptrue% |
31 \isamarkuptrue% |
32 \isamarkupfalse% |
|
33 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula% |
32 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula% |
34 \begin{isamarkuptext}% |
33 \begin{isamarkuptext}% |
35 \noindent |
34 \noindent |
36 which stands for ``\emph{A}lways in the \emph{F}uture'': |
35 which stands for ``\emph{A}lways in the \emph{F}uture'': |
37 on all infinite paths, at some point the formula holds. |
36 on all infinite paths, at some point the formula holds. |
49 extended by new constructors or equations. This is just a trick of the |
48 extended by new constructors or equations. This is just a trick of the |
50 presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define |
49 presentation (see \S\ref{sec:doc-prep-suppress}). In reality one has to define |
51 a new datatype and a new function.}% |
50 a new datatype and a new function.}% |
52 \end{isamarkuptext}% |
51 \end{isamarkuptext}% |
53 \isamarkuptrue% |
52 \isamarkuptrue% |
54 \isamarkupfalse% |
|
55 \isamarkupfalse% |
|
56 {\isachardoublequoteopen}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequoteclose}% |
53 {\isachardoublequoteopen}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequoteclose}% |
57 \begin{isamarkuptext}% |
54 \begin{isamarkuptext}% |
58 \noindent |
55 \noindent |
59 Model checking \isa{AF} involves a function which |
56 Model checking \isa{AF} involves a function which |
60 is just complicated enough to warrant a separate definition:% |
57 is just complicated enough to warrant a separate definition:% |
67 \noindent |
64 \noindent |
68 Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that includes |
65 Now we define \isa{mc\ {\isacharparenleft}AF\ f{\isacharparenright}} as the least set \isa{T} that includes |
69 \isa{mc\ f} and all states all of whose direct successors are in \isa{T}:% |
66 \isa{mc\ f} and all states all of whose direct successors are in \isa{T}:% |
70 \end{isamarkuptext}% |
67 \end{isamarkuptext}% |
71 \isamarkuptrue% |
68 \isamarkuptrue% |
72 \isamarkupfalse% |
|
73 \isamarkupfalse% |
|
74 {\isachardoublequoteopen}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
69 {\isachardoublequoteopen}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
75 \begin{isamarkuptext}% |
70 \begin{isamarkuptext}% |
76 \noindent |
71 \noindent |
77 Because \isa{af} is monotone in its second argument (and also its first, but |
72 Because \isa{af} is monotone in its second argument (and also its first, but |
78 that is irrelevant), \isa{af\ A} has a least fixed point:% |
73 that is irrelevant), \isa{af\ A} has a least fixed point:% |
96 {\isafoldproof}% |
91 {\isafoldproof}% |
97 % |
92 % |
98 \isadelimproof |
93 \isadelimproof |
99 % |
94 % |
100 \endisadelimproof |
95 \endisadelimproof |
101 \isamarkupfalse% |
96 % |
102 % |
97 \isadelimproof |
103 \isadelimproof |
98 % |
104 % |
99 \endisadelimproof |
105 \endisadelimproof |
100 % |
106 % |
101 \isatagproof |
107 \isatagproof |
102 % |
108 \isamarkupfalse% |
103 \endisatagproof |
109 \isamarkupfalse% |
104 {\isafoldproof}% |
110 % |
105 % |
111 \endisatagproof |
106 \isadelimproof |
112 {\isafoldproof}% |
107 % |
113 % |
108 \endisadelimproof |
114 \isadelimproof |
109 % |
115 % |
110 \isadelimproof |
116 \endisadelimproof |
111 % |
117 \isamarkupfalse% |
112 \endisadelimproof |
118 % |
113 % |
119 \isadelimproof |
114 \isatagproof |
120 % |
|
121 \endisadelimproof |
|
122 % |
|
123 \isatagproof |
|
124 \isamarkupfalse% |
|
125 \isamarkupfalse% |
|
126 \isamarkupfalse% |
|
127 \isamarkupfalse% |
|
128 \isamarkupfalse% |
|
129 \isamarkupfalse% |
|
130 \isamarkupfalse% |
|
131 \isamarkupfalse% |
|
132 \isamarkupfalse% |
|
133 \isamarkupfalse% |
|
134 \isamarkupfalse% |
|
135 \isamarkupfalse% |
|
136 \isamarkupfalse% |
|
137 \isamarkupfalse% |
|
138 % |
115 % |
139 \endisatagproof |
116 \endisatagproof |
140 {\isafoldproof}% |
117 {\isafoldproof}% |
141 % |
118 % |
142 \isadelimproof |
119 \isadelimproof |
390 \end{isabelle} |
367 \end{isabelle} |
391 is extensionally equal to \isa{path\ s\ Q}, |
368 is extensionally equal to \isa{path\ s\ Q}, |
392 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}.% |
369 where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}.% |
393 \end{isamarkuptext}% |
370 \end{isamarkuptext}% |
394 \isamarkuptrue% |
371 \isamarkuptrue% |
395 \isamarkupfalse% |
372 % |
396 % |
373 \isadelimproof |
397 \isadelimproof |
374 % |
398 % |
375 \endisadelimproof |
399 \endisadelimproof |
376 % |
400 % |
377 \isatagproof |
401 \isatagproof |
|
402 \isamarkupfalse% |
|
403 \isamarkupfalse% |
|
404 \isamarkupfalse% |
|
405 \isamarkupfalse% |
|
406 \isamarkupfalse% |
|
407 \isamarkupfalse% |
|
408 \isamarkupfalse% |
|
409 \isamarkupfalse% |
|
410 \isamarkupfalse% |
|
411 \isamarkupfalse% |
|
412 \isamarkupfalse% |
|
413 \isamarkupfalse% |
|
414 \isamarkupfalse% |
|
415 \isamarkupfalse% |
|
416 \isamarkupfalse% |
|
417 % |
378 % |
418 \endisatagproof |
379 \endisatagproof |
419 {\isafoldproof}% |
380 {\isafoldproof}% |
420 % |
381 % |
421 \isadelimproof |
382 \isadelimproof |
516 \isacommand{consts}\isamarkupfalse% |
477 \isacommand{consts}\isamarkupfalse% |
517 \ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
478 \ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
518 \isacommand{primrec}\isamarkupfalse% |
479 \isacommand{primrec}\isamarkupfalse% |
519 \isanewline |
480 \isanewline |
520 {\isachardoublequoteopen}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline |
481 {\isachardoublequoteopen}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline |
521 {\isachardoublequoteopen}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequoteclose}\isamarkupfalse% |
482 {\isachardoublequoteopen}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequoteclose}% |
522 % |
|
523 \begin{isamarkuptext}% |
483 \begin{isamarkuptext}% |
524 \noindent |
484 \noindent |
525 Expressing the semantics of \isa{EU} is now straightforward: |
485 Expressing the semantics of \isa{EU} is now straightforward: |
526 \begin{isabelle}% |
486 \begin{isabelle}% |
527 \ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ f{\isacharbraceright}\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ g{\isacharbraceright}\ s\ p{\isacharparenright}% |
487 \ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ f{\isacharbraceright}\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ g{\isacharbraceright}\ s\ p{\isacharparenright}% |
544 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}. |
504 %which enables you to read and write {text"E[f U g]"} instead of {term"EU f g"}. |
545 \end{exercise} |
505 \end{exercise} |
546 For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.% |
506 For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.% |
547 \end{isamarkuptext}% |
507 \end{isamarkuptext}% |
548 \isamarkuptrue% |
508 \isamarkuptrue% |
549 \isamarkupfalse% |
509 % |
550 \isamarkupfalse% |
510 \isadelimproof |
551 % |
511 % |
552 \isadelimproof |
512 \endisadelimproof |
553 % |
513 % |
554 \endisadelimproof |
514 \isatagproof |
555 % |
515 % |
556 \isatagproof |
516 \endisatagproof |
557 \isamarkupfalse% |
517 {\isafoldproof}% |
558 \isamarkupfalse% |
518 % |
559 \isamarkupfalse% |
519 \isadelimproof |
560 \isamarkupfalse% |
520 % |
561 \isamarkupfalse% |
521 \endisadelimproof |
562 \isamarkupfalse% |
522 % |
563 \isamarkupfalse% |
523 \isadelimproof |
564 % |
524 % |
565 \endisatagproof |
525 \endisadelimproof |
566 {\isafoldproof}% |
526 % |
567 % |
527 \isatagproof |
568 \isadelimproof |
528 % |
569 % |
529 \endisatagproof |
570 \endisadelimproof |
530 {\isafoldproof}% |
571 \isamarkupfalse% |
531 % |
572 % |
532 \isadelimproof |
573 \isadelimproof |
533 % |
574 % |
534 \endisadelimproof |
575 \endisadelimproof |
535 % |
576 % |
536 \isadelimproof |
577 \isatagproof |
537 % |
578 \isamarkupfalse% |
538 \endisadelimproof |
579 \isamarkupfalse% |
539 % |
580 \isamarkupfalse% |
540 \isatagproof |
581 % |
|
582 \endisatagproof |
|
583 {\isafoldproof}% |
|
584 % |
|
585 \isadelimproof |
|
586 % |
|
587 \endisadelimproof |
|
588 \isamarkupfalse% |
|
589 % |
|
590 \isadelimproof |
|
591 % |
|
592 \endisadelimproof |
|
593 % |
|
594 \isatagproof |
|
595 \isamarkupfalse% |
|
596 \isamarkupfalse% |
|
597 \isamarkupfalse% |
|
598 \isamarkupfalse% |
|
599 \isamarkupfalse% |
|
600 \isamarkupfalse% |
|
601 \isamarkupfalse% |
|
602 \isamarkupfalse% |
|
603 \isamarkupfalse% |
|
604 \isamarkupfalse% |
|
605 \isamarkupfalse% |
|
606 % |
541 % |
607 \endisatagproof |
542 \endisatagproof |
608 {\isafoldproof}% |
543 {\isafoldproof}% |
609 % |
544 % |
610 \isadelimproof |
545 \isadelimproof |
629 \isadelimtheory |
564 \isadelimtheory |
630 % |
565 % |
631 \endisadelimtheory |
566 \endisadelimtheory |
632 % |
567 % |
633 \isatagtheory |
568 \isatagtheory |
634 \isamarkupfalse% |
|
635 % |
569 % |
636 \endisatagtheory |
570 \endisatagtheory |
637 {\isafoldtheory}% |
571 {\isafoldtheory}% |
638 % |
572 % |
639 \isadelimtheory |
573 \isadelimtheory |