Constraint-Based Abstract Semantics for Temporal Logic

A Direct Approach to Design and Implementation

Gourinath Banda, John Patrick Gallagher

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

Resumé

Abstract interpretation provides a practical approach to verifying properties of infinite-state systems. We apply the framework of abstract interpretation to derive an abstract semantic function for the modal mu-calculus, which is the basis for abstract model checking. The abstract semantic function is constructed directly from the standard concrete semantics together with a Galois connection between the concrete state-space and an abstract domain. There is no need for mixed or modal transition systems to abstract arbitrary temporal properties, as in previous work in the area of abstract model checking. Using the modal mu-calculus to implement CTL, the abstract semantics gives an over-approximation of the set of states in which an arbitrary CTL formula holds. Then we show that this leads directly to an effective implementation of an abstract model checking algorithm for CTL using abstract domains based on linear constraints. The implementation of the abstract semantic function makes use of an SMT solver. We describe an implemented system for proving properties of linear hybrid automata and give some experimental results.
OriginalsprogEngelsk
TitelLogic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, Dakar, Senegal,
RedaktørerEdmund M. Clarke, Andrei Voronkov
Antal sider19
ForlagSpringer
Publikationsdato30 nov. 2010
Sider27-45
ISBN (Trykt)978-3-642-17510-7
StatusUdgivet - 30 nov. 2010
BegivenhedInternational Conference on Logic for Programming Artificial Intelligence and Reasoning - Dakar, Senegal
Varighed: 25 apr. 20101 maj 2010

Konference

KonferenceInternational Conference on Logic for Programming Artificial Intelligence and Reasoning
LandSenegal
ByDakar
Periode25/04/201001/05/2010
NavnLecture Notes in Computer Science
Vol/bind6355
ISSN0302-9743

Citer dette

Banda, G., & Gallagher, J. P. (2010). Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation. I E. M. Clarke, & A. Voronkov (red.), Logic for Programming, Artificial Intelligence, and Reasoning: 16th International Conference, LPAR-16, Dakar, Senegal, (s. 27-45). Springer. Lecture Notes in Computer Science, Bind. 6355
Banda, Gourinath ; Gallagher, John Patrick. / Constraint-Based Abstract Semantics for Temporal Logic : A Direct Approach to Design and Implementation. Logic for Programming, Artificial Intelligence, and Reasoning: 16th International Conference, LPAR-16, Dakar, Senegal,. red. / Edmund M. Clarke ; Andrei Voronkov. Springer, 2010. s. 27-45 (Lecture Notes in Computer Science, Bind 6355).
@inproceedings{dd4db03561cc48f2872fafc713d601c2,
title = "Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation",
abstract = "Abstract interpretation provides a practical approach to verifying properties of infinite-state systems. We apply the framework of abstract interpretation to derive an abstract semantic function for the modal mu-calculus, which is the basis for abstract model checking. The abstract semantic function is constructed directly from the standard concrete semantics together with a Galois connection between the concrete state-space and an abstract domain. There is no need for mixed or modal transition systems to abstract arbitrary temporal properties, as in previous work in the area of abstract model checking. Using the modal mu-calculus to implement CTL, the abstract semantics gives an over-approximation of the set of states in which an arbitrary CTL formula holds. Then we show that this leads directly to an effective implementation of an abstract model checking algorithm for CTL using abstract domains based on linear constraints. The implementation of the abstract semantic function makes use of an SMT solver. We describe an implemented system for proving properties of linear hybrid automata and give some experimental results.",
author = "Gourinath Banda and Gallagher, {John Patrick}",
year = "2010",
month = "11",
day = "30",
language = "English",
isbn = "978-3-642-17510-7",
pages = "27--45",
editor = "Clarke, {Edmund M.} and Andrei Voronkov",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning",
publisher = "Springer",

}

Banda, G & Gallagher, JP 2010, Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation. i EM Clarke & A Voronkov (red), Logic for Programming, Artificial Intelligence, and Reasoning: 16th International Conference, LPAR-16, Dakar, Senegal,. Springer, Lecture Notes in Computer Science, bind 6355, s. 27-45, International Conference on Logic for Programming Artificial Intelligence and Reasoning, Dakar, Senegal, 25/04/2010.

Constraint-Based Abstract Semantics for Temporal Logic : A Direct Approach to Design and Implementation. / Banda, Gourinath; Gallagher, John Patrick.

Logic for Programming, Artificial Intelligence, and Reasoning: 16th International Conference, LPAR-16, Dakar, Senegal,. red. / Edmund M. Clarke; Andrei Voronkov. Springer, 2010. s. 27-45 (Lecture Notes in Computer Science, Bind 6355).

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - Constraint-Based Abstract Semantics for Temporal Logic

T2 - A Direct Approach to Design and Implementation

AU - Banda, Gourinath

AU - Gallagher, John Patrick

PY - 2010/11/30

Y1 - 2010/11/30

N2 - Abstract interpretation provides a practical approach to verifying properties of infinite-state systems. We apply the framework of abstract interpretation to derive an abstract semantic function for the modal mu-calculus, which is the basis for abstract model checking. The abstract semantic function is constructed directly from the standard concrete semantics together with a Galois connection between the concrete state-space and an abstract domain. There is no need for mixed or modal transition systems to abstract arbitrary temporal properties, as in previous work in the area of abstract model checking. Using the modal mu-calculus to implement CTL, the abstract semantics gives an over-approximation of the set of states in which an arbitrary CTL formula holds. Then we show that this leads directly to an effective implementation of an abstract model checking algorithm for CTL using abstract domains based on linear constraints. The implementation of the abstract semantic function makes use of an SMT solver. We describe an implemented system for proving properties of linear hybrid automata and give some experimental results.

AB - Abstract interpretation provides a practical approach to verifying properties of infinite-state systems. We apply the framework of abstract interpretation to derive an abstract semantic function for the modal mu-calculus, which is the basis for abstract model checking. The abstract semantic function is constructed directly from the standard concrete semantics together with a Galois connection between the concrete state-space and an abstract domain. There is no need for mixed or modal transition systems to abstract arbitrary temporal properties, as in previous work in the area of abstract model checking. Using the modal mu-calculus to implement CTL, the abstract semantics gives an over-approximation of the set of states in which an arbitrary CTL formula holds. Then we show that this leads directly to an effective implementation of an abstract model checking algorithm for CTL using abstract domains based on linear constraints. The implementation of the abstract semantic function makes use of an SMT solver. We describe an implemented system for proving properties of linear hybrid automata and give some experimental results.

M3 - Article in proceedings

SN - 978-3-642-17510-7

SP - 27

EP - 45

BT - Logic for Programming, Artificial Intelligence, and Reasoning

A2 - Clarke, Edmund M.

A2 - Voronkov, Andrei

PB - Springer

ER -

Banda G, Gallagher JP. Constraint-Based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation. I Clarke EM, Voronkov A, red., Logic for Programming, Artificial Intelligence, and Reasoning: 16th International Conference, LPAR-16, Dakar, Senegal,. Springer. 2010. s. 27-45. (Lecture Notes in Computer Science, Bind 6355).