Efficient algorithms and tools for MITL model-checking and synthesis

被引：3

作者：

Brihaye, Thomas ^{[1
]}

Geeraerts, Gilles ^{[2
]}

Ho, Hsi-Ming ^{[3
]}

Milchior, Arthur ^{[2
]}

Monmege, Benjamin ^{[4
,5
]}

机构：

[1] UMons, Mons, Belgium

[2] Univ Libre Bruxelles, Brussels, Belgium

[3] Univ Cambridge, Cambridge, England

[4] Aix Marseille Univ, CNRS, Marseille, France

[5] Univ Toulon & Var, LIS, La Garde, France

来源：

2018 23RD INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS) | 2018年

关键词：

MITL; Model-checking; Synthesis; Timed automata; LTL;

D O I：

10.1109/ICECCS2018.2018.00027

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Metric Interval Temporal Logic (MITL) is an extension of the classical Linear Time Logic (LTL) that can be used to characterise real-time properties of computer systems. While the practical interest of MITL is undeniable, there is still today a remarkable lack of tool support for this logic. In this short paper, we report on our on-going work effort to complete the theoretical knowledge about MITL. We also report on our recently introduced tool MightyL, which translates MITL formulae into timed automata, enabling efficient model checking of this logic. Finally, we sketch the future directions of our current line of research, which will be to extend MightyL to support reactive synthesis of MITL properties.

引用

页码：180 / 184

页数：5

共 50 条

[1] On Model-Checking Optimistic Replication Algorithms
Boucheneb, Hanifa
Imine, Abdessamad
[J]. FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2009, 5522 : 73 - +
[2] Saturation algorithms for model-checking pushdown systems
Carayol, Arnaud
Hague, Matthew
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (151): : 1 - 24
[3] Symbolic Model-Checking of Optimistic Replication Algorithms
Boucheneb, Hanifa
Imine, Abdessamad
Najem, Manal
[J]. INTEGRATED FORMAL METHODS, 2010, 6396 : 89 - +
[4] Efficient global model-checking for propositional μ-calculus
Jiang, Hua
[J]. Jisuanji Yanjiu yu Fazhan/Computer Research and Development, 2010, 47 (08): : 1424 - 1433
[5] Efficient CTL model-checking for pushdown systems
Song, Fu
Touili, Tayssir
[J]. THEORETICAL COMPUTER SCIENCE, 2014, 549 : 127 - 145
[6] Efficient CTL Model-Checking for Pushdown Systems
Song, Fu
Touili, Tayssir
[J]. CONCUR 2011: CONCURRENCY THEORY, 2011, 6901 : 434 - +
[7] Antichains: Alternative algorithms for LTL satisfiability and model-checking
De Wulf, M.
Doyen, L.
Maquet, N.
Raskin, J. -F.
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 63 - +
[8] Improved algorithms for the automata-based approach to model-checking
Doyen, Laurent
Raskin, Jean-Francois
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 451 - +
[9] Integration of model-checking tools: from Discrete to hybrid models
Mufti, Waseem A.
Tcherukine, Dimitri C.
[J]. INMIC 2007: PROCEEDINGS OF THE 11TH IEEE INTERNATIONAL MULTITOPIC CONFERENCE, 2007, : 106 - 109
[10] Efficient Parallel CTL Model-Checking for Pushdown Systems
Chen, Xinyu
Wei, Hansheng
Ye, Xin
Hao, Li
Huang, Yanhong
Shi, Jianqi
[J]. 2018 IEEE INT CONF ON PARALLEL & DISTRIBUTED PROCESSING WITH APPLICATIONS, UBIQUITOUS COMPUTING & COMMUNICATIONS, BIG DATA & CLOUD COMPUTING, SOCIAL COMPUTING & NETWORKING, SUSTAINABLE COMPUTING & COMMUNICATIONS, 2018, : 23 - 30

← 1 2 3 4 5 →