A Symbolic Model for Timed Concurrent Constraint Programming

作     者：Arias, Jaime Guzman, Michell Olarte, Carlos 

作者机构：Univ Bordeaux LaBRI UMR 5800 F-33400 Talence France CNRS LaBRI UMR 5800 F-33400 Talence France Univ Valle DECC Cali Colombia Univ Fed Rio Grande do Norte ECT BR-59072970 Natal RN Brazil Pontificia Univ Javeriana Cali DECC Cali Colombia 

出 版 物：《ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE》 (理论计算机科学电子札记)

年 卷 期：2015年第312卷

页      面：161-177页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：Concurrent constraint programming temporal logic model checking 

摘      要：Concurrent Constraint Programming (ccp) is a model for concurrency where agents interact with each other by telling and asking constraints (i. e., formulas in logic) into a shared store of partial information. The ntcc calculus extends ccp with the notion of discrete time-units for the specification of reactive systems. Moreover, ntcc features constructors for non-deterministic choices and asynchronous behavior, thus allowing for (1) synchronization of processes via constraint entailment during a time-unit and (2) synchronization of processes along time-intervals. In this paper we develop the techniques needed for the automatic verification of ntcc programs based on symbolic model checking. We show that the internal transition relation, modeling the behavior of processes during a time-unit (1 above), can be symbolically represented by formulas in a suitable fragment of linear time temporal logic. Moreover, by using standard techniques as difference decision diagrams, we provide a compact representation of these constraints. Then, relying on a fixpoint characterization of the timed constructs, we obtain a symbolic model of the observable transition (2 above). We prove that our construction is correct with respect to the operational semantics. Finally, we introduce a prototypical tool implementing our method.