Hostname: page-component-cd9895bd7-gbm5v Total loading time: 0 Render date: 2024-12-25T17:11:39.741Z Has data issue: false hasContentIssue false
  • English
  • Français

Abstract Diagnosis for tccp using a Linear Temporal Logic

Published online by Cambridge University Press:  21 July 2014

MARCO COMINI ,
LAURA TITOLO  and
ALICIA VILLANUEVA
MARCO COMINI
Affiliation:
DIMI, Università degli Studi di Udine, Italy (e-mail: [email protected])
LAURA TITOLO
Affiliation:
DIMI, Università degli Studi di Udine, Italy (e-mail: [email protected])
ALICIA VILLANUEVA
Affiliation:
DSIC, Universitat Politècnica de València, Spain (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

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.

Keywords

concurrent constraint paradigmlinear temporal logicabstract diagnosisdecision proceduresprogram verification
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 14 , Special Issue 4-5: 30th International Conference on Logic Programming , July 2014 , pp. 787 - 801
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Alpuente, M., Falaschi, M., and Villanueva, A. 2005a. A Symbolic Model Checker for tccp Programs. In First International Workshop on Rapid Integration of Software Engineering Techniques (RISE 2004), Revised Selected Papers. Lecture Notes in Computer Science, vol. 3475. Springer-Verlag, 45–56.Google Scholar
Alpuente, M., Gallardo, M., Pimentel, E., and Villanueva, A. 2005b. A Semantic Framework for the Abstract Model Checking of tccp Programs. Theoretical Computer Science 346, 1, 58–95.Google Scholar
Alpuente, M., Gallardo, M., Pimentel, E., and Villanueva, A. 2006. Verifying Real-Time Properties of tccp Programs. Journal of Universal Computer Science 12, 11, 1551–1573.Google Scholar
Clarke, E. M. and Emerson, E. A. 1982. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop. Springer-Verlag, London, UK, 52–71.Google Scholar
Comini, M., Titolo, L., and Villanueva, A. 2011. Abstract Diagnosis for Timed Concurrent Constraint programs. Theory and Practice of Logic Programming 11, 4-5, 487–502.CrossRefGoogle Scholar
Comini, M., Titolo, L., and Villanueva, A. 2013a. A Condensed Goal-Independent Bottom-Up Fixpoint Modeling the Behavior of tccp. Tech. rep., DSIC, Universitat Politècnica de València. Available at http://riunet.upv.es/handle/10251/34328.Google Scholar
Comini, M., Titolo, L., and Villanueva, A. 2013b. Towards an Effective Decision Procedure for LTL formulas with Constraints. In 23rd Workshop on Logic-based methods in Programming Environments (WLPE 2013). CoRR abs/1308.2055.Google Scholar
Comini, M., Titolo, L., and Villanueva, A. 2014. Abstract Diagnosis for tccp using a Linear Temporal Logic. Tech. rep., Universitat Politècnica de València. Available at http://riunet.upv.es/handle/10251/8351.Google Scholar
de Boer, F. S., Gabbrielli, M., and Meo, M. C. 2000. A Timed Concurrent Constraint Language. Information and Computation 161, 1, 45–83.Google Scholar
de Boer, F. S., Gabbrielli, M., and Meo, M. C. 2001. A Temporal Logic for Reasoning about Timed Concurrent Constraint Programs. In TIME '01: Proceedings of the Eighth International Symposium on Temporal Representation and Reasoning (TIME'01). IEEE Computer Society, Washington, DC, USA, 227.Google Scholar
de Boer, F. S., Gabbrielli, M., and Meo, M. C. 2002. Proving correctness of Timed Concurrent Constraint Programs. CoRR cs.LO/0208042.CrossRefGoogle Scholar
Falaschi, M., Olarte, C., Palamidessi, C., and Valencia, F. D. 2007. Declarative Diagnosis of Temporal Concurrent Constraint Programs. In Logic Programming, 23rd International Conference, ICLP 2007, Proceedings, Dahl, V. and Niemelä, I., Eds. Lecture Notes in Computer Science, vol. 4670. Springer-Verlag, 271–285.Google Scholar
Falaschi, M., Policriti, A., and Villanueva, A. 2001. Modeling concurrent systems specified in a temporal concurrent constraint language-I. Electronic Notes in Theoretical Computer Science 48, 197–210.Google Scholar
Falaschi, M. and Villanueva, A. 2006. Automatic verification of timed concurrent constraint programs. Theory and Practice of Logic Programming 6, 3, 265–300.CrossRefGoogle Scholar
Gaintzarain, J., Hermo, M., Lucio, P., and Navarro, M. 2008. Systematic semantic tableaux for PLTL. Electronic Notes in Theoretical Computer Science 206, 59–73.CrossRefGoogle Scholar
Gaintzarain, J., Hermo, M., Lucio, P., Navarro, M., and Orejas, F. 2009. Dual Systems of Tableaux and Sequents for PLTL. The Journal of Logic and Algebraic Programming 78, 8, 701–722.Google Scholar
Manna, Z. and Pnueli, A. 1992. The temporal logic of reactive and concurrent systems - specification. Springer.Google Scholar
Palamidessi, C. and Valencia, F. D. 2001. A Temporal Concurrent Constraint Programming Calculus. In 7th International Conference on Principles and Practice of Constraint Programming (CP'01). Lecture Notes in Computer Science, vol. 2239. Springer, 302–316.Google Scholar
Queille, J. P. and Sifakis, J. 1982. Specification and verification of concurrent systems in CESAR. In Symposium on Programming, Dezani-Ciancaglini, M. and Montanari, U., Eds. Lecture Notes in Computer Science, vol. 137. Springer, 337–351.CrossRefGoogle Scholar
Saraswat, V. A. 1989. Concurrent Constraint Programming Languages. Ph.D. thesis, Carnegie-Mellon University.CrossRefGoogle Scholar
Saraswat, V. A. 1993. Concurrent Constraint Programming. The MIT Press, Cambridge, Mass.CrossRefGoogle Scholar
Valencia, F. D. 2005. Decidability of infinite-state timed CCP processes and first-order LTL. Theoretical Computer Science 330, 3, 577–607.CrossRefGoogle Scholar