Specifying and Verifying External Behaviour of Fair Input/Output Automata by Using the Temporal Logic of Actions

被引：1
|
作者：
Kapus, Tatjana [1 ]
机构：
[1] Univ Maribor, Fac Elect Engn & Comp Sci, SI-2000 Maribor, Slovenia
来源：
INFORMATICA | 2015年 / 26卷 / 04期
关键词：
formal specification; fair input/output automaton; temporal logic of actions; fair trace; fair trace inclusion;
D O I：
10.15388/Informatica.2015.71
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Fair input/output (or I/O) automata are a state-machine model for specifying and verifying reactive and concurrent systems. For the verification purposes, one is usually interested only in the sequences of interactions fair I/O automata offer to their environment. These sequences are called fair traces. The usual approach to the verification consists in proving fair trace inclusion between fair I/O automata. This paper presents a simple approach to the specification of fair traces and shows how to establish a fair trace inclusion relation for a pair of fair 110 automata by using the temporal logic of actions.
引用
收藏
页码：685 / 704
页数：20
相关论文
共 50 条
  • [21] Effective Characterizations of Simple Fragments of Temporal Logic Using Prophetic Automata
    Preugschat, Sebastian
    Wilke, Thomas
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, FOSSACS 2012, 2012, 7213 : 135 - 149
  • [22] Analysis of synchronous and asynchronous cellular automata using abstraction by temporal logic
    Hagiya, M
    Takahashi, K
    Yamamoto, M
    Sato, T
    FUNCTIONAL AND LOGIC PROGRAMMING, 2004, 2998 : 7 - 21
  • [23] Safety verification of model helicopter controller using hybrid input/output automata
    Mitra, S
    Wang, Y
    Lynch, N
    Feron, E
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2003, 2623 : 343 - 358
  • [24] Modeling and Verification of a Robotic Surgical System using Hybrid Input/Output Automata
    Capiluppi, Marta
    Schreiter, Luzie
    Fiorini, Paolo
    Raczkowsky, Joerg
    Woern, Heinz
    2013 EUROPEAN CONTROL CONFERENCE (ECC), 2013, : 4238 - 4243
  • [25] Constructing Buchi automata from linear temporal logic using simulation relations for alternating Buchi automata
    Fritz, C
    IMPLEMENTATION AND APPLICATION OF AUTOMATA, PROCEEDINGS, 2003, 2759 : 35 - 48
  • [26] Verifying Linear Temporal Logic Properties in UML/OCL Class Diagrams using Filmstripping
    Hilken, Frank
    Gogolla, Martin
    19TH EUROMICRO CONFERENCE ON DIGITAL SYSTEM DESIGN (DSD 2016), 2016, : 708 - 713
  • [27] Timed Automata Approach for Motion Planning Using Metric Interval Temporal Logic
    Zhou, Yuchen
    Maity, Dipankar
    Baras, John S.
    2016 EUROPEAN CONTROL CONFERENCE (ECC), 2016, : 690 - 695
  • [28] Model Checking Temporal-Epistemic Logic Using Alternating Tree Automata
    Belardinelli, Francesco
    Jones, Andrew V.
    Lomuscio, Alessio
    FUNDAMENTA INFORMATICAE, 2011, 112 (01) : 19 - 37
  • [29] Modeling System Safety Requirements Using Input/Output Constraint Meta-Automata
    Chen, Zhe
    Motet, Gilles
    2009 FOURTH INTERNATIONAL CONFERENCE ON SYSTEMS (ICONS), 2009, : 228 - 233
  • [30] Using Predicate Temporal Logic and Coloured Petri Nets to specifying integrity restrictions in the structural evolution of temporal active systems
    Rodríguez-Fortiz, MJ
    Parets-Llorca, J
    INTERNATIONAL SYMPOSIUM ON PRINCIPLES OF SOFTWARE EVOLUTION, PROCEEDINGS, 2000, : 83 - 87
12345