Model checking of CTL from 630 lecture

mc-ctl.rkt

#lang typed/racket

(define ∅ : (Setof Nothing) {set})
(define ∪ set-union)
(define ∩ set-intersect)
(define ∋ set-member?)

(: fix : (∀ (X) (X → X) X → X))
;; Compute `f`'s fixpoint starting from `x`
(define (fix f x)
  (let ([x* (f x)])
    (if (equal? x* x) x (fix f x*))))

;; Kripke structure
(struct (S A) M ([S : (Setof S)] ; Set of states
                 [R : (S → (Setof S))] ; transition
                 [ℓ : (S → (Setof A))] ; labelling
                 [I : S]) ; initial state
  #:transparent)

;; Positive normal form CTL parameterized by atom set `A`
(struct (A) Φ () #:transparent)
(struct (A) ι Φ ([a : A]) #:transparent)
(struct (A) ¬ Φ ([a : A]) #:transparent)
(struct (A) ∨ Φ ([l : (Φ A)] [r : (Φ A)]) #:transparent)
(struct (A) ∧ Φ ([l : (Φ A)] [r : (Φ A)]) #:transparent)
(struct (A) EX Φ ([Φ : (Φ A)]) #:transparent)
(struct (A) AX Φ ([Φ : (Φ A)]) #:transparent)
(struct (A) EU Φ ([l : (Φ A)] [r : (Φ A)]) #:transparent)
(struct (A) AU Φ ([l : (Φ A)] [r : (Φ A)]) #:transparent)
(struct (A) ER Φ ([l : (Φ A)] [r : (Φ A)]) #:transparent)
(struct (A) AR Φ ([l : (Φ A)] [r : (Φ A)]) #:transparent)
;; extra ones
(struct (A) EF Φ ([Φ : (Φ A)]) #:transparent)
(struct (A) AF Φ ([Φ : (Φ A)]) #:transparent)
(struct (A) EW Φ ([l : (Φ A)] [r : (Φ A)]) #:transparent)
(struct (A) AW Φ ([l : (Φ A)] [r : (Φ A)]) #:transparent)
(struct (A) AG Φ ([Φ : (Φ A)]) #:transparent)

(: ⟦_⟧M : (∀ (S A) (M S A) (Φ A) → (Setof S)))
;; Return all states in `M` satisfying `φ`
(define (⟦_⟧M m φ)
  (match-define (M S R ℓ _) m)

  ;; Least and most fix-points
  (define-syntax-rule (μ (X) e) (fix (λ ([X : (Setof S)]) e) ∅))
  (define-syntax-rule (ν (X) e) (fix (λ ([X : (Setof S)]) e) S))

  (: AX/S : (Setof S) → (Setof S))
  ;; `AX` on semantics instead of syntax
  (define (AX/S S′)
    (for/set: : (Setof S) ([s S] #:when (for/and : Boolean ([s′ (R s)]) (∋ S′ s′)))
      s))

  (: EX/S : (Setof S) → (Setof S))
  ;; `EX` on semantics instead of syntax
  (define (EX/S S′)
    (for/set: : (Setof S) ([s S] #:when (for/or : Boolean ([s′ (R s)]) (∋ S′ s′)))
      s))

  ;; Main loop
  (let ⟦_⟧ : (Setof S) ([φ : (Φ A) φ])
    (match φ
      [(ι a) (for/set: : (Setof S) ([s S] #:when (∋ (ℓ s) a)) s)]
      [(¬ a) (for/set: : (Setof S) ([s S] #:unless (∋ (ℓ s) a)) s)]
      [(∨ φ₁ φ₂) (∪ (⟦_⟧ φ₁) (⟦_⟧ φ₂))]
      [(∧ φ₁ φ₂) (∩ (⟦_⟧ φ₁) (⟦_⟧ φ₂))]
      [(EX φ) (EX/S (⟦_⟧ φ))]
      [(AX φ) (AX/S (⟦_⟧ φ))]
      [(AG φ) (ν (X) (∩ (⟦_⟧ φ) (AX/S X)))]
      [(EF φ) (μ (X) (∪ (⟦_⟧ φ) (EX/S X)))]
      [(AF φ) (μ (X) (∪ (⟦_⟧ φ) (AX/S X)))]
      [(EU φ₁ φ₂) (μ (X) (∪ (⟦_⟧ φ₂) (∩ (⟦_⟧ φ₁) (EX/S X))))]
      [(AU φ₁ φ₂) (μ (X) (∪ (⟦_⟧ φ₂) (∩ (⟦_⟧ φ₁) (AX/S X))))]
      [(EW φ₁ φ₂) (ν (X) (∪ (⟦_⟧ φ₂) (∩ (⟦_⟧ φ₁) (EX/S X))))]
      [(AW φ₁ φ₂) (ν (X) (∪ (⟦_⟧ φ₂) (∩ (⟦_⟧ φ₁) (AX/S X))))]
      [(ER φ₁ φ₂)
       (let ([S₁ (⟦_⟧ φ₁)]
             [S₂ (⟦_⟧ φ₂)])
         (ν (X) (∪ (∩ S₁ S₂) (∩ S₂ (EX/S X)))))]
      [(AR φ₁ φ₂)
       (let ([S₁ (⟦_⟧ φ₁)]
             [S₂ (⟦_⟧ φ₂)])
         (ν (X) (∪ (∩ S₁ S₂) (∩ S₂ (AX/S X)))))])))

(: ⊨ : (∀ (S A) (M S A) (Φ A) → Boolean))
;; Model-check `m` against `φ`
(define (⊨ m φ) (∋ (⟦_⟧M m φ) (M-I m)))


;; White-board example
(define m
  (M (set 0 1 2 3)
     (match-lambda
       [0 (set 1 3)]
       [1 (set 1 2)]
       [2 (set 2)]
       [3 (set 3)])
     (match-lambda
       [0 (set 'a)]
       [1 (set 'a)]
       [2 (set 'b)]
       [3 (set 'a)])
     0))
(⟦_⟧M m (EU (ι 'a) (ι 'b)))
(⟦_⟧M m (AU (ι 'a) (ι 'b)))
(⟦_⟧M m (ER (ι 'b) (ι 'a)))