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 条
  • [41] On-line monitoring of metric temporal logic with time-series constraints using alternating finite automata
    Drusinsky, Doron
    JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2006, 12 (05) : 482 - 498
  • [42] Towards a model of input-output behaviour of wastewater treatment plants using soft computing techniques
    Belanche, LA
    Valdés, JJ
    Comas, J
    Roda, IR
    Poch, M
    ENVIRONMENTAL MODELLING & SOFTWARE, 1999, 14 (05) : 409 - 419
  • [43] Power Management System for Multi-input Multi-output Energy Harvesters using Fuzzy Logic
    Porras, Carl Justin Vincent G.
    Santiago, Gianne Klarisse Q.
    Soriano, Katrina Ysabel M.
    Sumabat, Cara Martha R.
    Albao, Justine D.
    Dela Cruz, Angelo R.
    Vicerra, Ryan Rhay P.
    Roxas, Edison A.
    2015 INTERNATIONAL CONFERENCE ON HUMANOID, NANOTECHNOLOGY, INFORMATION TECHNOLOGY,COMMUNICATION AND CONTROL, ENVIRONMENT AND MANAGEMENT (HNICEM), 2015, : 556 - +
  • [44] Using a temporal input-output approach to analyze the ripple effect of China's energy consumption
    Cheng Yongwei
    Mu Dong
    Ren Huanyu
    Fan Tijun
    Du Jianbang
    ENERGY, 2020, 211 (211)
  • [45] Measurement of the efficiency of a Multi–Input–Multi–Output (MIMO) production process using transfer function and fuzzy logic
    Francis Ikechukwu Obidike
    Chidozie Chukwuemeka Nwobi-Okoye
    OPSEARCH, 2023, 60 : 1976 - 2000
  • [46] Modelling the performance of single-input-single-output (SISO) processes using transfer function and fuzzy logic
    Nwobi-Okoye, Chidozie Chukwuemeka
    OPSEARCH, 2020, 57 (03) : 815 - 836
  • [47] Reinforcement Learning of Control Policy for Linear Temporal Logic Specifications Using Limit-Deterministic Generalized Buchi Automata
    Oura, Ryohei
    Sakakibara, Ami
    Ushio, Toshimitsu
    IEEE CONTROL SYSTEMS LETTERS, 2020, 4 (03): : 761 - 766
  • [48] Modelling the performance of single-input–single-output (SISO) processes using transfer function and fuzzy logic
    Chidozie Chukwuemeka Nwobi-Okoye
    OPSEARCH, 2020, 57 : 815 - 836
  • [49] Measurement of the efficiency of a Multi-Input-Multi-Output (MIMO) production process using transfer function and fuzzy logic
    Obidike, Francis Ikechukwu
    Nwobi-Okoye, Chidozie Chukwuemeka
    OPSEARCH, 2023, 60 (04) : 1976 - 2000
  • [50] Ride comfort improvement using robust multi-input multi-output fuzzy logic dynamic compensator
    Ozbek, Cengiz
    Ozguney, Omur Can
    Burkan, Recep
    Yagiz, Nurkan
    PROCEEDINGS OF THE INSTITUTION OF MECHANICAL ENGINEERS PART I-JOURNAL OF SYSTEMS AND CONTROL ENGINEERING, 2023, 237 (01) : 72 - 85
12345