Help us understand the problem. What is going on with this article?

Scalaでモデル検査器を書いてみた

数理論理学AdC2019 15日目の記事です。
大学の授業でScalaを学んでいるので、その練習のためにCTLという時相論理で動くような簡単なモデル検査プログラムを書いてみたという話です。
ここに載せてあるコードはすべて私のGitHubにあります。

CTLについて

CTLとはComputional Tree Logic(計算木論理)のことであり、Kripkeモデルに対して、そこでの経路に対する言明についても表すことができる時相論理の一種である。

CTLの構文論

CTLの論理式は状態に対して真偽が定まる状態論理式と、パスという状態の無限列について真偽が定まるパス論理式の二つがあり、BNFで以下のように定義されている。

状態論理式の文法

$P$を原子論理式、$\psi$を後述するパス論理式として

 \phi ::= \top \ |\ \bot \ |\ P \ |\ \lnot \phi\ |\ \phi \lor \phi\ |\ \phi \land \phi \ |\  \phi \rightarrow \phi\ |\ \phi \leftrightarrow \phi \ |\ A\psi\ |\ E\psi

$A$や$E$はパス演算子と呼ばれるもので、その状態から始まるすべての(ある)パスで$\psi$が成り立つことを表す。

パス論理式の文法

$\phi$を状態論理式として

\psi ::= X\phi\ |\ F\phi\ |\ G\phi\ |\ \phi_1U\phi_2\ |\ \phi_1R\phi_2\ 

$X,F,G,U,R$は時相演算子と呼ばれるもので、パス上でどのように$\phi$が満たされるかを定めるものである。

実装

これらの文法をScalaコードで表すと以下のようになる。

formula.scala
// 状態論理式
trait StateFml
case object True extends StateFml
case object False extends StateFml
case class Prop(name: String) extends StateFml
case class Not(e: StateFml) extends StateFml
case class And(e1: StateFml, e2: StateFml) extends StateFml // e1 /\ e2
case class Or(e1: StateFml, e2: StateFml) extends StateFml  // e1 \/ e2
case class Imp(e1: StateFml, e2: StateFml) extends StateFml // e1 => e2 
case class Eq(e1: StateFml, e2: StateFml) extends StateFml // e1 <=> e2

// パス論理式
trait PassFml
case class X(e: StateFml) extends PassFml
case class F(e: StateFml) extends PassFml
case class G(e: StateFml) extends PassFml
case class U(e1: StateFml, e2: StateFml) extends PassFml
case class R(e1: StateFml, e2: StateFml) extends PassFml

// パス演算子
case class A(e: PassFml) extends StateFml
case class E(e: PassFml) extends StateFml

CTLの意味論

Kripkeモデル

状態遷移をグラフ$(W, R)$で表し、これをKripkeフレームという。ただし後述する検査アルゴリズムの都合上ここでは$W$も$R$も有限なものとする。

さらに遷移系で調べたい性質を原子論理式で表して、その集合を$P$とする。これらの真偽は状態ごとに定まっているので解釈$V$を

 V\colon W \times P \rightarrow \{True, False\}

として与え、これらの組(W,R,V)をKripkeモデルという。

また、Kripkeフレーム上のパスとは状態の列

\pi = w_0, w_1,w_2,... 

であって、$\forall i \in \mathbb{N}\ w_i \in W\land (w_i, w_{i+1})\in R$をみたすものをいう。

状態論理式の解釈

Kripkeモデル$M = (W,R,V)$が与えられているとして、$w \in W$をその中の状態とする。この下での状態論理式の解釈を以下で与える。

$M, w\models \top$
$M, w\not\models \ \bot$
$M, w\models p\ (p \in P) :\Longleftrightarrow V(w, p) = True$
$M, w\models \lnot \phi :\Longleftrightarrow M, w\models \phi\ が成立しない$
$M, w\models \phi_1 \lor \phi_2 :\Longleftrightarrow M, w\models \phi_1\ または\ M, w\models \phi_2$
$M, w\models \phi_1 \land \phi_2 :\Longleftrightarrow M, w\models \phi_1\ かつ\ M, w\models \phi_2$
$M, w\models \phi_1 \rightarrow \phi_2 :\Longleftrightarrow M, w\models \phi_1\ が成立するならば\ M, w\models \phi_2\ も成り立つ$
$ M, w\models \phi_1 \leftrightarrow \phi_2 :\Longleftrightarrow M, w\models \phi_1 \rightarrow \phi_2\ かつ\ M, w\models \phi_2 \rightarrow \phi_1$
$M, w\models A\psi :\Longleftrightarrow\ wから始まる任意のパス\piで\ M, \pi\models \psi$
$M, w\models E\psi :\Longleftrightarrow\ wから始まるあるパス\piで\ M, \pi\models \psi$

パス論理式の解釈

$M$をKripkeモデル$\pi = w_0, w_1, ...$をパスとして、この下でのパス論理式の解釈を以下で与える。

$M, \pi \models X\phi :\Longleftrightarrow M,w_1 \models\phi$
$M, \pi \models F\phi :\Longleftrightarrow あるk\geq0が存在してM,w_k \models\phi$
$M, \pi \models G\phi :\Longleftrightarrow 任意のk\geq0についてM,w_k \models\phi$
$M, \pi \models \phi_1U\phi_2 :\Longleftrightarrow あるk\geq0が存在して、M,w_k \models\phi_2であり任意のi\in[0,k-1]についてM,w_i \models\phi_1$
$M, \pi \models \phi_1R\phi_2 :\Longleftrightarrow 任意のk\geq0に対し、M,w_k\models\phi_2 であるかあるi\in[0,k-1]についてM,w_i\models\phi_1$

実装

Kripkeモデルのクラスを用意し、モデル検査用のメソッドcheckとその補助関数(satisfy, reach)を用意し、これらの計算に必要な前処理をコンストラクタで行うようにした。makeRevGraphではRの逆向きのグラフを作り、makeSCCではKripkeフレームでの強連結成分分解を行っている。

kripke.scala
class KripkeModel[Q] (nodes: Set[Q], edge: Map[Q, Set[Q]], valuation: Map[(Q, String), Boolean]){
  // 前処理
  // 反対向きのグラフを生成
  def makeRevGraph: Map[Q, Set[Q]] = {
    ...
  }
  val redge = makeRevGraph.withDefaultValue(Set())

  // 強連結成分分解
  def makeSCC: (Int, Map[Int, Set[Int]], Map[Int, Set[Q]]) = { // ノード数, 辺, Idからそれを指すQの集合への写像
    ...
  }
  val (sccSize, edgeSCC, idToQ) = makeSCC

// モデル検査用のメソッド群
  def satisfy (q: Q, fml: StateFml): Boolean = fml match {
    ...
  }

  def reach (fml: StateFml, target: Set[Q]) : Set[Q] = {
    ...
  }

  def check (fml: StateFml): Set[Q] = fml match {
    ...
  }
}

モデル検査アルゴリズム

Kripkeモデル$M = (W, R, V)$を固定したときに、次のようなものを計算する関数$check$を考える。

入力:状態論理式$\phi$
出力:$M, w\models \phi$を満たす状態$w$の集合$Q\subset W$

基本的には最後に適用した演算子で場合分けして、再帰的に計算していけばよい。ここでは直接$check$を求めるのではなく、状態論理式$\phi$と状態$w$を受け取って$M,w\models \phi$かを求める補助関数$satisfy$を使って$filter$で集めるようにした。(ただ一部の場合はcheckから求める方が楽なのでそうなっている)

// 充足判定
  def satisfy (q: Q, fml: StateFml): Boolean = fml match {
    case True => true
    case False => false
    case Prop(str) => valuation.getOrElse((q, str), false)
    case Not(e) => !satisfy(q, e)
    case And(e1, e2) => satisfy(q, e1) & satisfy(q, e2)
    case Or(e1, e2) => satisfy(q, e1) || satisfy(q, e2)
    case Imp(e1, e2) => satisfy(q, Not(e1)) || satisfy(q, e2)
    case Eq(e1, e2) => satisfy(q, Imp(e1, e2)) && satisfy(q, Imp(e2, e1))
    // パス演算子を含む場合はこれから
    case A(F(e)) => ...
    ...
}
def check (fml: StateFml): Set[Q] = fml match {
    // パス演算子を含む場合はこれから
    case E(U(e1, e2)) => ...
    case A(U(e1, e2)) => ...
    ...
    // 充足する状態をWの中からfilterで絞る
    case _ => nodes.filter(satisfy(_, fml))
}

面倒なのがパス演算子(AとE)が含まれる時で、その内側にある時相演算子(X,F,G,U,R)を含めれば10通りの場合分けが必要であるが、定義の意味を考えると、

  • $AX\phi$ と $\lnot EX\lnot\phi$
  • $EF\phi$ と $E(\top U\phi)$
  • $AG\phi$ と $\lnot EF\lnot \phi$
  • $AF\phi$ と $\lnot EG\lnot\phi$
  • $A(\phi_1U\phi_2)$ と $\lnot E(\lnot \phi_2U(\lnot \phi_1 \land \lnot \phi_2)) \land \lnot EG\lnot \phi_2$
  • $A(\phi_1R\phi_2)$ と $\lnot E(\lnot\phi_1U\lnot\phi_2)$
  • $E(\phi_1R\phi_2)$ と $\lnot A(\lnot\phi_1U\lnot\phi_2)$

が等価であることがわかり(証明略)、実際に計算しないといけないものは

  • $EX\phi$
  • $EG\phi$
  • $E\phi_1U\phi_2$

の三つであることがわかる。

EXの場合

$M, w\models EX\phi \Longleftrightarrowある(w, x) \in RについてM, x\models \phi$
となるので$w$から出ている辺をすべて調べればよい。

EUの場合

$\phi_2$を満たすような状態$w$固定してそこまで$\phi_1$を満たしながらたどり着ける状態をすべて足していけば$check(E\phi_1U\phi_2)$が直接求められる

EGの場合

$W, R$は有限なので、$\phi$をずっと満たす無限パスは、$\phi$をずっと満たすようなサイクルの中を回っているはずなので、そのような強連結成分と、そこに$\phi$をみたしながらたどり着ける状態たちを求めればいい。
前者には強連結成分分解というアルゴリズムを使い、後者はEUの時と同じアルゴリズムを使って求めればいい。

最後にこれらのすべてを実装すると以下のようになる。

Kripke.scala
class KripkeModel[Q] (nodes: Set[Q], edge: Map[Q, Set[Q]], valuation: Map[(Q, String), Boolean]){
  // 前処理
  // 反対向きのグラフを生成
  def makeRevGraph: Map[Q, Set[Q]] = {
    var e = Map[Q, Set[Q]]()    
    for((from, to) <- edge) {
      for (i <- to) {
       if(e.contains(i)){
         e += (i -> (e(i) + from))
        }else {
         e += (i -> Set(from))
        }
      }
    }
    e
  }
  val redge = makeRevGraph.withDefaultValue(Set())

  // 強連結成分分解
  def makeSCC: (Int, Map[Int, Set[Int]], Map[Int, Set[Q]]) = { // ノード数, 辺, Idからそれを指すQの集合への写像
    var used = Set[Q]()
    var ls = List[Q]()

    // 一回目のdfsでトポロジカルソート
    def dfs(q: Q): Unit = {
      used += q
      val qto = edge.getOrElse(q, Set())
      for (next <- qto) {
        if(!used(next)) {
          dfs(next)
        }
      }
      ls :+= q
    }
    for (q <- nodes) {
      if(!used(q)) {
        dfs(q)
      }
    }
    used = Set()
    // 二回目のdfsで辺を張る
    var edgeSCC = Map[Int, Set[Int]]().withDefaultValue(Set())
    var idToNodes = Map[Int, Set[Q]]().withDefaultValue(Set())
    var nodeToID = Map[Q, Int]()
    var id = 0
    def rdfs(q: Q, id: Int): Unit = {
      used += q
      nodeToID += (q -> id)
      idToNodes += (id -> (idToNodes(id) + q)) // これはひどい
      val qto = redge.getOrElse(q, Set())
      for (next <- qto){
        if(used(next)) {
          val idfrom = nodeToID(q)
          val idto = nodeToID(next)
          if(idfrom != idto) {
            edgeSCC += (idto -> (edgeSCC(idfrom) + idfrom))  // これはひどい
          }
        }else {
          rdfs(next, id)
        }
      }
    }
    for (q <- ls.reverse) {
      if(!used(q)) {
        rdfs(q, id)
        id += 1
      }
    }
    (id, edgeSCC, idToNodes)
  }
  val (sccSize, edgeSCC, idToQ) = makeSCC

  // 充足判定
  def satisfy (q: Q, fml: StateFml): Boolean = fml match {
    case True => true
    case False => false
    case Prop(str) => valuation.getOrElse((q, str), false)
    case Not(e) => !satisfy(q, e)
    case And(e1, e2) => satisfy(q, e1) & satisfy(q, e2)
    case Or(e1, e2) => satisfy(q, e1) || satisfy(q, e2)
    case Imp(e1, e2) => satisfy(q, Not(e1)) || satisfy(q, e2)
    case Eq(e1, e2) => satisfy(q, Imp(e1, e2)) && satisfy(q, Imp(e2, e1))
    case A(X(e)) => satisfy(q, (Not(E(X(Not(e))))))
    case E(X(e)) => {
      var ans = false
      for (q1 <- edge.getOrElse(q, Set())) {
        ans |= satisfy(q1, e)
      }
      ans
    }
    case A(F(e)) => !satisfy(q, E(G(Not(e))))
    case E(F(e)) => satisfy(q, E(U(True, e)))
    case A(G(e)) => !satisfy(q, E(F(Not(e))))
    case E(G(e)) => check(fml).contains(q)    
    case A(U(e1, e2)) => !satisfy(q, E(U(Not(e2), And(Not(e1), Not(e2))))) && !satisfy(q, E(G(Not(e2))))
    case E(U(e1, e2)) => check(fml).contains(q)
    case A(R(e1, e2)) => !satisfy(q, E(U(Not(e1), Not(e2))))
    case E(R(e1, e2)) => !satisfy(q, A(U(Not(e1), Not(e2))))
  }

  def reach (fml: StateFml, target: Set[Q]) : Set[Q] = {
    var ans = target
    var tmp = ans // targetにたどり着いていて、それまでのパス上でfmlを充足するものの集合
    var next: Set[Q] = Set()
    while (!tmp.isEmpty) {
      next = Set()
      for (s <- tmp) {
        val go_s = redge(s) // R(t, s)なるt全体
        for (t <- go_s) {
          if (!ans(t) && satisfy(t, fml)) {
            ans += t
            next += t 
          }
        }
      }
      tmp = next
    }
    ans
  }

  def check (fml: StateFml): Set[Q] = fml match {
    case E(U(e1, e2)) => reach(e1, check(e2))
    case E(G(e)) => {
      var sccs = Set[Q]()
      for (i <- 0 to sccSize - 1) {
        val sets = idToQ(i)
        if (sets.forall(satisfy(_, e))){
          sccs = sccs ++ sets
        }
      }
      reach(e, sccs)
    }
    case _ => nodes.filter(satisfy(_, fml))
  }
}

おわりに

いかがだったでしょうか、正直汚くて読みづらいコードを書いている自覚はあります…
関数型言語でグラフアルゴリズムを実装することに慣れていなかったので、mutableなデータ構造を使いまくって手続き型のように書いてしまったのもよくないなあと思ってます。
ただ一度動いたものを書き直すのはめんどくさい…

参考文献

蓮尾『モデル検査入門』:記事の大部分はこのpdfを参考に書きました
萩谷・西崎『論理と計算のしくみ』:ロジック部分で参考にしました
蟻本:強連結成分分解で参考にしました

jgvt5ti
理論計算機科学と形式手法が好きです
https://strtbox.hatenablog.com/
Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
Comments
No comments
Sign up for free and join this conversation.
If you already have a Qiita account
Why do not you register as a user and use Qiita more conveniently?
You need to log in to use this function. Qiita can be used more conveniently after logging in.
You seem to be reading articles frequently this month. Qiita can be used more conveniently after logging in.
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
ユーザーは見つかりませんでした