The automata-theoretic approach to verification of reactive systems

被引：0
作者：
Chebotarev A.N. [1 ]
机构：
[1] Cybernetics Institute, National Academy of Sciences of Ukraine, Kiev
来源：
Cybernetics and Systems Analysis | 2001年 / 37卷 / 6期
关键词：
Construction of automata from formulas; Formulas of temporal logics; Reactive systems; Reduction and verification of automata; Verification of reactive systems;
D O I：
10.1023/A:1014573629895
中图分类号：
学科分类号：
摘要：
Basic problems related to the use of automata-theoretic methods of verification of reactive systems are considered; in particular, the constmction of an automaton from a formula of a temporal logic and the reduction of the automaton being verified are described. ©2001 Plenum Publishing Corporation.
引用
收藏
页码：810 / 819
页数：9
相关论文
共 11 条
  • [1] Clarke E.M., Emerson E.A., Design and synthesis of synchronization skeletons using branching time temporal logic,, LNCS, 131, pp. 52-71, (1981)
  • [2] Emerson E.A., Lei C.L., Modalities for model checking: Branching time logic strikes back,, In: Proc. Twelfth ACM Symp. on Principles of Programming Languages, pp. 84-96, (1985)
  • [3] Sistla A.P., Clarke E.M., The complexity of prepositional linear temporal logics,, J. ACM, 32, 3, pp. 733-749, (1985)
  • [4] Kurshan R.P., Computer-Aided Verification of Coordinating Processes: the Automata-Theoretic Approach, (1994)
  • [5] Chebotarev A.N., Provably-correct development of reactive algorithms,, Proc. Int. Workshop on Rewriting Techniques and Efficient Theorem Proving, pp. 117-133, (2000)
  • [6] Chebotarev A.N., Construction of an automaton from a formula of the monadic first-order theory of natural numbers,, Kibem. Sist. Anal., No., 4, pp. 91-106, (2001)
  • [7] McMillan K.L., Symbolic Model Checking, (1994)
  • [8] Clarke E.M., Long O.E., McMillan K.L., Compositional model checking,, Proc. Forth Annual IEEE Symp. on Logic in Computer Sei., (1989)
  • [9] Graf S., Steffen B., Compositional minimization of finite state systems,, LNCS, 531, pp. 186-196, (1991)
  • [10] Ben-Ari M., Mathematical Logic for Computer Science, (1993)
12