Abstract diagnosis for tccp using a linear temporal logic

DOI10.1017/S1471068414000349MaRDI QIDQ2931280zbMATH OpenFDO

Authors Laura Titolo, A. Villanueva, Marco Comini

Publication date 25 November 2014

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1405.3675

zbMATH Keywords

abstract diagnosisdecision procedureslinear temporal logicprogram verificationtimed concurrent constraint paradigm

Mathematics Subject Classification ID

Temporal logic (03B44) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which represents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and sometimes the needed fragment is quite huge. In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpretation techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.

Recommendations

• Abstract model checking of \textsf{tccp} programs
• A semantic framework for the abstract model checking of tccp programs
• scientific article; zbMATH DE number 177234
• Declarative Diagnosis of Temporal Concurrent Constraint Programs
• Automatic verification of timed concurrent constraint programs

Cites work

• A semantic framework for the abstract model checking of tccp programs
• A timed concurrent constraint language.
• Abstract diagnosis for timed concurrent constraint programs
• Automatic verification of timed concurrent constraint programs
• Decidability of infinite-state timed CCP processes and first-order LTL
• Dual systems of tableaux and sequents for PLTL
• Modeling concurrent systems specified in a temporal concurrent constraint language. I

This page was built for publication: Abstract diagnosis for tccp using a linear temporal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2931280)