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 条
  • [1] Specifying and verifying interaction protocols in a temporal action logic
    Dipartimento di Informatica, Università del Piemonte Orientale, Alessandria, Italy
    不详
    不详
    J. Appl. Logic, 2007, 2 (214-234):
  • [2] Specifying and verifying systems of communicating agents in a temporal action logic
    Giordano, L
    Martelli, A
    Schwind, C
    AI(ASTERISK)IA 2003: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2003, 2829 : 262 - 274
  • [3] Specifying and verifying temporal behavior of high assurance systems using reachability tree logic
    Yang, SJH
    Chu, W
    Lin, S
    Lee, J
    THIRD IEEE INTERNATIONAL HIGH-ASSURANCE SYSTEMS ENGINEERING SYMPOSIUM, PROCEEDINGS, 1998, : 150 - 156
  • [4] Specifying and verifying temporal behavior of high assurance systems using reachability tree logic
    Yang, SJH
    Chu, W
    Lee, J
    INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING, 1999, 9 (02) : 233 - 249
  • [5] Specifying Timed Patterns using Temporal Logic
    Ulus, Dogan
    Maler, Oded
    HSCC 2018: PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (PART OF CPS WEEK), 2018, : 167 - 176
  • [6] Specifying and Verifying Communications Protocols using Mixed Intuitionistic Linear Logic
    Sinclair, David
    Power, James
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 133 : 255 - 273
  • [7] VERIFYING RECURSIVE SUBPROGRAMS USING TEMPORAL LOGIC
    KAPLAN, SM
    JOURNAL OF SYMBOLIC LOGIC, 1987, 52 (01) : 324 - 325
  • [8] A temporal logic for input output symbolic transition systems
    Aiguier, M
    Gaston, C
    Le Gall, P
    Longuet, D
    Touil, A
    12TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 2005, : 43 - 50
  • [9] Specifying User Preferences Using Weighted Signal Temporal Logic
    Mehdipour, Noushin
    Vasile, Cristian-Ioan
    Belta, Calin
    IEEE CONTROL SYSTEMS LETTERS, 2021, 5 (06): : 2006 - 2011
  • [10] Specifying User Preferences using Weighted Signal Temporal Logic
    Mehdipour, Noushin
    Vasile, Cristian-Ioan
    Belta, Calin
    2021 AMERICAN CONTROL CONFERENCE (ACC), 2021, : 4900 - 4905
12345