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 条
  • [31] Verifying Vaccine Supply Chain System in Indonesia Using Linear-Time Temporal Logic
    Wikatama, Muhammad Fikri Suyudi
    Arzaki, Muhammad
    Rusmawati, Yanti
    2018 6TH INTERNATIONAL CONFERENCE ON INFORMATION AND COMMUNICATION TECHNOLOGY (ICOICT), 2018, : 245 - 253
  • [32] EFFECTIVE CHARACTERIZATIONS OF SIMPLE FRAGMENTS OF TEMPORAL LOGIC USING CARTON-MICHEL AUTOMATA
    Preugschat, Sebastian
    Wilke, Thomas
    LOGICAL METHODS IN COMPUTER SCIENCE, 2013, 9 (02)
  • [33] Integration of Corporate Electronic Services into a Smart Space Using Temporal Logic of Actions
    Levonevskiy, Dmitriy
    Vatamaniuk, Irina
    Saveliev, Anton
    INTERACTIVE COLLABORATIVE ROBOTICS (ICR 2017), 2017, 10459 : 134 - 143
  • [34] A Novel Design of 3 Input 8 Output Decoder Using Quantum Dot Cellular Automata
    Banerjee, Sumanta
    Mondal, Sourav
    Bhattacharya, Jayanta
    Bandyopadhyay, Rounak
    Chatterjee, Ritika
    Dutta, Rajat
    Bagchi, Prateek
    Das, Pritam
    7TH IEEE ANNUAL INFORMATION TECHNOLOGY, ELECTRONICS & MOBILE COMMUNICATION CONFERENCE IEEE IEMCON-2016, 2016,
  • [35] A Formal Model of Quorum Based k-Mutex Algorithm using Input/Output Automata
    Nur, Ismail M.
    Lawi, Armin
    2016 INTERNATIONAL CONFERENCE ON COMPUTATIONAL INTELLIGENCE AND CYBERNETICS, 2016, : 109 - 113
  • [36] An input-output simulation approach to controlling multi-affine systems for linear temporal logic specifications
    Sun, Yajuan
    Lin, Hai
    Chen, Ben M.
    INTERNATIONAL JOURNAL OF CONTROL, 2012, 85 (10) : 1464 - 1476
  • [37] USING INPUT OUTPUT LEONTIEF MODEL IN HIGHER EDUCATION BASED ON KNOWLEDGE ENGINEERING AND FUZZY LOGIC
    Perez Gama, Jesus Alfonso
    Remolina Caro, Carlos Hernan
    Caro Gomez, Claudia Lucia
    Hoyos Gomez, Guillermo
    Mena Mena, Alexis
    PROCEEDINGS OF 2016 IEEE GLOBAL ENGINEERING EDUCATION CONFERENCE (EDUCON2016), 2016, : 1056 - 1064
  • [38] Multi input single output control of viscous fluid flow using fuzzy logic controller
    Matheen, R. Abdul
    2006 IEEE International Conference on Industrial Technology, Vols 1-6, 2006, : 925 - 930
  • [39] Engaging More Students in Formal Methods Education: A Practical Approach Using Temporal Logic of Actions
    Laufer, Konstantin
    Mertin, Gunda
    Thiruvathukal, George K.
    COMPUTER, 2024, 57 (12) : 118 - 123
  • [40] Reliable coplanar full adder in quantum-dot cellular automata using five-input majority logic
    Vanaraj, Anantharaj Thalaimalai
    Raj, Marshal
    Gopalakrishnan, Lakshminarayanan
    JOURNAL OF NANOPHOTONICS, 2020, 14 (02)
12345