مؤتمر
Checking interval properties of computations
| العنوان: | Checking interval properties of computations |
|---|---|
| المؤلفون: | Montanari A., Murano A., Perelli G., Peron A. |
| المساهمون: | Combi C., Cesta A., Laroussinie F., Montanari, A., Murano, A., Perelli, G., Peron, A. |
| بيانات النشر: | Institute of Electrical and Electronics Engineers Inc. 10662 LOS VAQUEROS CIRCLE, PO BOX 3014, LOS ALAMITOS, CA 90720-1264 USA |
| سنة النشر: | 2014 |
| المجموعة: | Sapienza Università di Roma: CINECA IRIS |
| مصطلحات موضوعية: | interval temporal logic, model checking, Kripke structure, complexity |
| الوصف: | Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g. A Kripke structure, and a formula specifying its expected behavior, one can verify whether the system meets the behavior by checking the formula against the model. Classically, system behavior is given as a formula of a temporal logic, such as LTL and the like. These logics are 'point-wise' interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those involving temporal aggregations, which are inherently 'interval-based', and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham's interval temporal logic HS over Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against Kripke structures is decidable by a suitable small model theorem, and we outline a PSpace decision procedure for the meaningful fragments AAbarBBbar and AAbarEEbar. |
| نوع الوثيقة: | conference object |
| اللغة: | English |
| العلاقة: | info:eu-repo/semantics/altIdentifier/isbn/978-1-4799-4227-5; info:eu-repo/semantics/altIdentifier/isbn/978-1-4799-4228-2; info:eu-repo/semantics/altIdentifier/wos/WOS:000349455500006; ispartofbook:2014 21st International Symposium on Temporal Representation and Reasoning; 21st International Symposium on Temporal Representation and Reasoning, TIME 2014; firstpage:59; lastpage:68; numberofpages:10; serie:PROCEEDINGS - INTERNATIONAL WORKSHOP ON TEMPORAL REPRESENTATION AND REASONING; http://hdl.handle.net/11573/1403133Test; info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-84909634551 |
| DOI: | 10.1109/TIME.2014.24 |
| الإتاحة: | https://doi.org/10.1109/TIME.2014.24Test http://hdl.handle.net/11573/1403133Test |
| حقوق: | info:eu-repo/semantics/closedAccess |
| رقم الانضمام: | edsbas.F84E4696 |
| قاعدة البيانات: | BASE |
| DOI: | 10.1109/TIME.2014.24 |
|---|