Parameterized verification of monotone information systems

被引：0
|
作者：
Chane-Yack-Fa, Raphael [1 ]
Frappier, Marc [1 ]
Mammar, Amel [2 ]
Finkel, Alain [3 ,4 ]
机构：
[1] Univ Sherbrooke, Fac Sci, Dept Informat, GRIL, Sherbrooke, PQ, Canada
[2] SAMOVAR CNRS, Telecom SudParis, Evry, France
[3] Univ Paris Saclay, CNRS, LSV, Paris, France
[4] Univ Paris Saclay, ENS Paris Saclay, Paris, France
来源：
FORMAL ASPECTS OF COMPUTING | 2018年 / 30卷 / 3-4期
基金：
加拿大自然科学与工程研究理事会;
关键词：
Model checking; Parameterized verification; Process algebra; Well-structured transition systems; Well-quasi-ordering; Coverability; Information systems; INFINITE-STATE SYSTEMS; MODEL CHECKING; PROCESS ALGEBRA; DECIDABILITY; STATECHARTS; CUTOFF;
D O I：
10.1007/s00165-018-0460-8
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
In this paper, we study the information system verification problem as a parameterized verification one. Informations systems are modeled as multi-parameterized systems in a formal language based on the Algebraic State-Transition Diagrams (ASTD) notation. Then, we use the Well Structured Transition Systems (WSTS) theory to solve the coverability problem for an unbounded ASTD state space. Moreover, we define a new framework to prove the effective pred-basis condition of WSTSs, i.e. the computability of a base of predecessors for every states.
引用
收藏
页码：463 / 489
页数：27
相关论文
共 50 条
  • [41] Completely inapproximable monotone and antimonotone parameterized problems
    Marx, Daniel
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2013, 79 (01) : 144 - 151
  • [42] Environment abstraction for parameterized verification
    Clarke, E
    Talupur, M
    Veith, H
    VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2006, 3855 : 126 - 141
  • [43] Completely inapproximable monotone and antimonotone parameterized problems
    Marx, Daniel
    25TH ANNUAL IEEE CONFERENCE ON COMPUTATIONAL COMPLEXITY - CCC 2010, 2010, : 181 - 187
  • [44] Monotonic Abstraction in Parameterized Verification
    Abdulla, Parosh Aziz
    Delzanno, Giorgio
    Rezine, Ahmed
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 223 (0C) : 3 - 14
  • [45] Automated Parameterized Verification of CRDTs
    Nagar, Kartik
    Jagannathan, Suresh
    COMPUTER AIDED VERIFICATION, CAV 2019, PT II, 2019, 11562 : 459 - 477
  • [46] Parameterized verification by probabilistic abstraction
    Arons, T
    Pnueli, A
    Zuck, L
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2003, 2620 : 87 - 102
  • [47] Parameterized Verification of Transactional Memories
    Emmi, Michael
    Majumdar, Rupak
    Manevich, Roman
    PLDI '10: PROCEEDINGS OF THE 2010 ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, 2010, : 134 - 145
  • [48] Parameterized Verification of Transactional Memories
    Emmi, Michael
    Majumdar, Rupak
    Manevich, Roman
    ACM SIGPLAN NOTICES, 2010, 45 (06) : 134 - 145
  • [49] Characterization, verification and computation of robust controlled invariants for monotone dynamical systems
    Adnane Saoud
    Murat Arcak
    Mathematics of Control, Signals, and Systems, 2024, 36 (1) : 71 - 100
  • [50] Characterization, verification and computation of robust controlled invariants for monotone dynamical systems
    Saoud, Adnane
    Arcak, Murat
    MATHEMATICS OF CONTROL SIGNALS AND SYSTEMS, 2024, 36 (01) : 71 - 100
12345