Optimal Proofs for Linear Temporal Logic on Lasso Words

被引：10

作者：

Basin, David ^{[1
]}

Bhatt, Bhargav Nagaraja ^{[1
]}

Traytel, Dmitriy ^{[1
]}

机构：

[1] Swiss Fed Inst Technol, Dept Comp Sci, Inst Informat Secur, Zurich, Switzerland

来源：

AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2018) | 2018年 / 11138卷

基金：

瑞士国家科学基金会;

关键词：

MODEL CHECKING; LTL;

D O I：

10.1007/978-3-030-01090-4_3

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

YCounterexamples produced by model checkers can be hard to grasp. Often it is not even evident why a trace violates a specification. We show how to provide easy-to-check evidence for the violation of a linear temporal logic (LTL) formula on a lasso word, based on a novel sound and complete proof system for LTL on lasso words. Valid proof trees in our proof system follow the syntactic structure of the formula and provide insight on why each Boolean or temporal operator is violated or satisfied. We introduce the notion of optimal proofs with respect to a user-specified preference order and identify sufficient conditions for efficiently computing optimal proofs. We design and evaluate an algorithm that performs this computation, demonstrating that it can produce optimal proofs for complex formulas in under a second.

引用

页码：37 / 55

页数：19

共 27 条

[1] An operational semantics for Stateflow [J].

Grégoire Hamon ;

John Rushby .

International Journal on Software Tools for Technology Transfer, 2007, 9 (5-6) :447-456

[2]

[Anonymous], 1992, TEMPORAL LOGIC REACT, DOI DOI 10.1007/978-1-4612-0931-7

[3]

[Anonymous], 2018, NUSMV NEW SYMBOLIC M

[4]

[Anonymous], 2018, EXPLANATOR SEND EXPL

[5] From symptom to cause: Localizing errors in counterexample traces [J].

Ball, T ;

Naik, M ;

Rajamani, SK .

ACM SIGPLAN NOTICES, 2003, 38 (01) :97-105

[6] Explaining counterexamples using causality [J].

Beer, Ilan ;

Ben-David, Shoham ;

Chockler, Hana ;

Orni, Avigail ;

Trefler, Richard .

FORMAL METHODS IN SYSTEM DESIGN, 2012, 40 (01) :20-40

[7] Cut-free sequent systems for temporal logic [J].

Bruennler, Kai ;

Lange, Martin .

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2008, 76 (02) :216-225

[8]

Cheney J., 2009, TRENDS DATABASES, V1, P379

[9]

Cini Clare, 2015, Tools and Algorithms for the Construction and Analysis of Systems. 21st International Conference, TACAS 2015, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015. Proceedings: LNCS 9035, P581, DOI 10.1007/978-3-662-46681-0_54

[10] SORTING AND SELECTION IN POSETS [J].

Daskalakis, Constantinos ;

Karp, Richard M. ;

Mossel, Elchanan ;

Riesenfeld, Samantha J. ;

Verbin, Elad .

SIAM JOURNAL ON COMPUTING, 2011, 40 (03) :597-622

← 1 2 3 →