Modal Extensions of the Logic of Abstract State Machines

被引:0
作者
Ferrarotti, Flavio [1 ]
Schewe, Klaus-Dieter [1 ]
机构
[1] Software Competence Ctr Hagenberg, Hagenberg, Austria
来源
RIGOROUS STATE-BASED METHODS, ABZ 2024 | 2024年 / 14759卷
关键词
Abstract State Machines; temporal logic; liveness conditions; completeness; verification; mutual exclusion; LIVENESS PROPERTIES;
D O I
10.1007/978-3-031-63790-2_8
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Based on the logic of non-deterministic Abstract State Machines (ASMs) we define a modal extension ML ASM by first introducing multi-step predicates and then adding quantification over the number of steps. We show that liveness conditions such as invariance, conditional and unconditional progress, and persistence on all or some runs of an ASM can be expressed in this logic. We show the existence of a complete fragment of MLASM, which still contains the interesting liveness conditions, and demonstrate the usefulness of this complete fragment by an example concerning mutual exclusion.
引用
收藏
页码:123 / 140
页数:18
相关论文
共 50 条
[41]   Revisiting bisimilarity and its modal logic for nondeterministic and probabilistic processes [J].
Bernardo, Marco ;
De Nicola, Rocco ;
Loreti, Michele .
ACTA INFORMATICA, 2015, 52 (01) :61-106
[42]   A Formal Approach for Failure Detection in Large-Scale Distributed Systems Using Abstract State Machines [J].
Buga, Andreea ;
Nemes, Sorana Tania .
DATABASE AND EXPERT SYSTEMS APPLICATIONS, DEXA 2017, PT I, 2017, 10438 :505-513
[43]   View integration in data warehouse design using typed Abstract State Machines and strong data refinement [J].
Ma, Hui ;
Schewe, Klaus-Dieter ;
Zhao, Jane .
QSIC 2006: SIXTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, PROCEEDINGS, 2006, :175-+
[44]   Formal Verification of Generalised State Machines [J].
Eleftherakis, George ;
Kefalas, Petros .
PCI 2008: 12TH PAN-HELLENIC CONFERENCE ON INFORMATICS, PROCEEDINGS, 2008, :227-231
[45]   Model checking of hierarchical state machines [J].
Alur, R ;
Yannakakis, M .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001, 23 (03) :273-303
[46]   A PROPOSITIONAL MODAL LOGIC OF TIME INTERVALS [J].
HALPERN, JY ;
SHOHAM, Y .
JOURNAL OF THE ACM, 1991, 38 (04) :935-962
[47]   Free Choice in Modal Inquisitive Logic [J].
Karl Nygren .
Journal of Philosophical Logic, 2023, 52 :347-391
[48]   The modal logic of the countable random frame [J].
Goranko, V ;
Kapron, B .
ARCHIVE FOR MATHEMATICAL LOGIC, 2003, 42 (03) :221-243
[49]   Timing in music and modal temporal logic [J].
Marsden, Alan .
JOURNAL OF MATHEMATICS AND MUSIC, 2007, 1 (03) :173-189
[50]   Free Choice in Modal Inquisitive Logic [J].
Nygren, Karl .
JOURNAL OF PHILOSOPHICAL LOGIC, 2023, 52 (02) :347-391