From model-checking to temporal logic constraint solving

François Fages; Aurélien Rizk

doi:10.1007/978-3-642-04244-7_26

From model-checking to temporal logic constraint solving

François Fages
, Aurélien Rizk

École Polytechnique

INRIA Institut National de Recherche en Informatique et en Automatique

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

In this paper, we show how model-checking can be generalized to temporal logic constraint solving, by considering temporal logic formulae with free variables over some domain , and by computing a validity domain for the variables rather than a truth value for the formula. This allows us to define a continuous degree of satisfaction for a temporal logic formula in a given structure, opening up the field of model-checking to optimization. We illustrate this approach with reverse-engineering problems coming from systems biology, and provide some performance figures on parameter optimization problems with respect to temporal logic specifications.

Original language	English
Title of host publication	Principles and Practice of Constraint Programming - CP 2009 - 15th International Conference, CP 2009, Proceedings
Pages	319-334
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-04244-7_26
Publication status	Published - 2 Nov 2009
Event	15th International Conference on Principles and Practice of Constraint Programming, CP 2009 - Lisbon, Portugal Duration: 20 Sept 2009 → 24 Sept 2009

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5732 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	15th International Conference on Principles and Practice of Constraint Programming, CP 2009
Country/Territory	Portugal
City	Lisbon
Period	20/09/09 → 24/09/09

Access to Document

10.1007/978-3-642-04244-7_26

Cite this

Fages, F., & Rizk, A. (2009). From model-checking to temporal logic constraint solving. In Principles and Practice of Constraint Programming - CP 2009 - 15th International Conference, CP 2009, Proceedings (pp. 319-334). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5732 LNCS). https://doi.org/10.1007/978-3-642-04244-7_26

@inproceedings{7e8bdb55804245ed97ac4b98d297eba2,

title = "From model-checking to temporal logic constraint solving",

abstract = "In this paper, we show how model-checking can be generalized to temporal logic constraint solving, by considering temporal logic formulae with free variables over some domain , and by computing a validity domain for the variables rather than a truth value for the formula. This allows us to define a continuous degree of satisfaction for a temporal logic formula in a given structure, opening up the field of model-checking to optimization. We illustrate this approach with reverse-engineering problems coming from systems biology, and provide some performance figures on parameter optimization problems with respect to temporal logic specifications.",

author = "Fran{\c c}ois Fages and Aur{\'e}lien Rizk",

year = "2009",

month = nov,

day = "2",

doi = "10.1007/978-3-642-04244-7\_26",

language = "English",

isbn = "3642042430",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "319--334",

booktitle = "Principles and Practice of Constraint Programming - CP 2009 - 15th International Conference, CP 2009, Proceedings",

note = "15th International Conference on Principles and Practice of Constraint Programming, CP 2009 ; Conference date: 20-09-2009 Through 24-09-2009",

}

Fages, F & Rizk, A 2009, From model-checking to temporal logic constraint solving. in Principles and Practice of Constraint Programming - CP 2009 - 15th International Conference, CP 2009, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5732 LNCS, pp. 319-334, 15th International Conference on Principles and Practice of Constraint Programming, CP 2009, Lisbon, Portugal, 20/09/09. https://doi.org/10.1007/978-3-642-04244-7_26

From model-checking to temporal logic constraint solving. / Fages, François; Rizk, Aurélien.
Principles and Practice of Constraint Programming - CP 2009 - 15th International Conference, CP 2009, Proceedings. 2009. p. 319-334 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5732 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - From model-checking to temporal logic constraint solving

AU - Fages, François

AU - Rizk, Aurélien

PY - 2009/11/2

Y1 - 2009/11/2

N2 - In this paper, we show how model-checking can be generalized to temporal logic constraint solving, by considering temporal logic formulae with free variables over some domain , and by computing a validity domain for the variables rather than a truth value for the formula. This allows us to define a continuous degree of satisfaction for a temporal logic formula in a given structure, opening up the field of model-checking to optimization. We illustrate this approach with reverse-engineering problems coming from systems biology, and provide some performance figures on parameter optimization problems with respect to temporal logic specifications.

AB - In this paper, we show how model-checking can be generalized to temporal logic constraint solving, by considering temporal logic formulae with free variables over some domain , and by computing a validity domain for the variables rather than a truth value for the formula. This allows us to define a continuous degree of satisfaction for a temporal logic formula in a given structure, opening up the field of model-checking to optimization. We illustrate this approach with reverse-engineering problems coming from systems biology, and provide some performance figures on parameter optimization problems with respect to temporal logic specifications.

UR - https://www.scopus.com/pages/publications/70350424435

U2 - 10.1007/978-3-642-04244-7_26

DO - 10.1007/978-3-642-04244-7_26

M3 - Conference contribution

AN - SCOPUS:70350424435

SN - 3642042430

SN - 9783642042430

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 319

EP - 334

BT - Principles and Practice of Constraint Programming - CP 2009 - 15th International Conference, CP 2009, Proceedings

T2 - 15th International Conference on Principles and Practice of Constraint Programming, CP 2009

Y2 - 20 September 2009 through 24 September 2009

ER -

Fages F, Rizk A. From model-checking to temporal logic constraint solving. In Principles and Practice of Constraint Programming - CP 2009 - 15th International Conference, CP 2009, Proceedings. 2009. p. 319-334. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-04244-7_26

From model-checking to temporal logic constraint solving

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this