A.3 CWB-NC について
A.3.2 等価性の判定
trace等価性 AとBのtrace等価性を以下のコマンドで確認できる eq -S trace A B
弱双模倣性 AとBの弱双模倣性（あるいは観測等価性)を以下のコマンドで確認できる eq -S obseq A B
default 等価性指示子を省略するとデフォルトは，弱双模倣性（観測等価性）が選択される．
例えば，以下のセッションのように，SpecとSysの間の観測透過性を検査すると，Sys が[pub]<pub>ttを充足しないと表示される，これはCTMがteaを選択した場合に，デッ ドロックが発生するからである．
一方trace等価性ならば，受理するトレース（デッドロックは含まない）は同じなので，
等価であると判定される．
¶ ³
cwb-nc> eq Spec Sys Building automaton...
States: 6 Transitions: 6
Done building automaton.
Transforming automaton...
Done transforming automaton.
FALSE...
Spec satisfies:
[[pub]]<<pub>>tt Sys does not.
Execution time (user,system,gc,real):(0.047,0.000,0.000,0.047)
cwb-nc> eq -S trace Spec Sys Building automaton...
States: 6 Transitions: 6
Done building automaton.
Transforming automaton...
Done transforming automaton.
TRUE
Execution time (user,system,gc,real):(0.000,0.000,0.000,0.000)
µ ´
A.3.3 様相論理と到達可能性判定
様相論理をもちいた，到達可能性の判定もできる．CWBではHML式にて様相論理を表 現する．
例えば，いかなるアクションをも実行不能である状況を以下のcan_deadlockという命 題で表現することができる．[-]ffは全てのアクションがまったく実行できない状況を表
し，この状態に到達するかどうかを再帰的にXは定義している．minは最小不動点演算に 関係する．
¶ ³
prop can_deadlock = min X = [-]ff \/ <->X
µ ´
命題が定義できれば，プロセスに対して命題が成立する場合に到達可能であるかを判定 できる．いまcan_deadlockをファイル”dead.mu”に保存してあるものとして，上記Sys がデッドロック状況に到達可能であるかどうかを判定する．
¶ ³
cwb-nc> load dead.mu
cwb-nc> search Sys can_deadlock Building automaton...
States: 5 Transitions: 5
Done building automaton.
States explored: 1
State found satisfying can_deadlock.
Path to state contains 1 states, invoking simulator.
1: Sys cwb-nc-sim>
µ ´
充足可能であること，すなわちデッドロックに到達可能であることがわかる．
今度は，teeを出力しない自販機CMとの組合せに対してデッドロックを判定する
¶ ³
proc SmUni = (CM | CS) \ {coin, coffee}
µ ´
¶ ³
cwb-nc> search SmUni can_deadlock Building automaton...
States: 4 Transitions: 4
Done building automaton.
Building automaton...
States: 3 ...略...
States explored: 4
No state found satisfying can_deadlock.
µ ´
すなわち，SmUniに対してはdeadlockに到達可能でないことがわかる．
このように，CCSに従ってプロセスを定義し，透過性を検証し，また様相論理式をもち いて性質を定義して，充足性を判定できる．
参考文献
[1] The concurrency workbench of the new century. http://www.cs.sunysb.edu/˜cwb.
[2] L. Aceto, A. Ingolfsdottir, and J. Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
[3] R. Alur, K. Etessami, and M. Yannakakis. Inference of message sequence charts.
Software Engineering, IEEE Transactions on, 29(7):623–633, 2003.
[4] J. C. M. Baeten. A brief history of process algebra. Theor. Comput. Sci., 335(2-3):131–146, 2005.
[5] JCM Baeten and JA Bergstra. Discrete time process algebra. Formal Aspects of Computing, 8(2):188–208, 1996.
[6] J.C.M. Baeten and W.P. Weijland. Process algebra. Cambridge University Press Cambridge, 1990.
[7] J.A. Bergstra and J.W. Klop. The Algebra of Recursively Defined Processes and the Algebra of Regular Processes. 1983.
[8] J.A. Bergstra and J.W. Klop. Process Algebra for Synchronous Communication.
Information and Control, 60(1-3):109–137, 1984.
[9] A. Church. Logic, arithmetic and automata. InProc. Internat. Congr. on Mathemat-ics, Moscow, 1963.
[10] E.M. Clarke, O. Grumberg, and D.A. Peled. Model checking. Springer, 1999.
[11] L. de Alfaro, L.D. da Silva, M. Faella, A. Legay, P. Roy, M. Sorea, et al. Sociable interfaces. Procedings of FROCOS, 5, 2005.
[12] EA Emerson, CS Jutla, and AP Sistla. On model-checking for fragments of t-calculus.
In CAV’93, volume 697, pages 385–396. Springer, 1993.
[13] W. Fokkink. Introduction to Process Algebra. Springer, 2000.
[14] D. Giannakopoulou, C.S. Pasareanu, and H. Barringer. Assumption generation for software component verification. InProceedings of the 17th IEEE international confer-ence on Automated software engineering, page 3. IEEE Computer Society Washington, DC, USA, 2002.
[15] E. Gradel, W. Thomas, and T. Wilke. Automata, logics, and infinite games. Springer, 2002.
[16] Y. Gurevich and L. Harrington. Trees, automata, and games. In Proceedings of the fourteenth annual ACM symposium on Theory of computing, pages 60–65. ACM New York, NY, USA, 1982.
[17] B. Jobstmann, S. Galler, M. Weiglhofer, and R. Bloem. Anzu: A tool for property synthesis. Lecture Notes in Computer Science, 4590:258, 2007.
[18] M.Iwamasa K.Yamamoto, T.Ishii. System Level Specification Synthesis-An Extended Message Sequence Chart based Approach-. The 13rd Workshop on Synthesis And System Integration of Mixed Information technologies(SASIMI), 2006.
[19] H. Liang, J. Dingel, and Z. Diskin. A comparative survey of scenario-based to state-based model synthesis approaches. Proceedings of the 2006 international workshop on Scenarios and state machines: models, algorithms, and tools, pages 5–12, 2006.
[20] R. Milner. A Calculus of Communicating Systems. LNCS 92 Springer-Verlag, 1980.
[21] M. Lange O. Friedmann. The pgsolver collection of parity game solvers. Technical report, Ludwig-Maximilians-Universit¨at M¨unchen,, 2009.
[22] N. Piterman, A. Pnueli, and Y. Sa’ar. Synthesis of reactive (1) designs. Lecture notes in computer science, 3855:364, 2006.