A Symbolic model for timed concurrent constraint programming

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...

ver descrição completa

Na minha lista:
Detalhes bibliográficos
Principais autores: Arias, Jaime, Guzman, Michell, Vega, Carlos Alberto Olarte
Formato: article
Idioma:English
Publicado em: Elsevier
Assuntos:
Concurrent constraint programming
Temporal logic
Model checking
Endereço do item:https://repositorio.ufrn.br/jspui/handle/123456789/29761
Tags: Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
id ri-123456789-29761
record_format dspace
spelling ri-123456789-297612020-08-02T07:54:43Z A Symbolic model for timed concurrent constraint programming Arias, Jaime Guzman, Michell Vega, Carlos Alberto Olarte 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 2020-07-30T19:15:42Z 2020-07-30T19:15:42Z 2015 article ARIAS, Jaime; GUZMÁN, Michell; OLARTE, Carlos. A Symbolic Model for Timed Concurrent Constraint Programming. Electronic Notes In Theoretical Computer Science, [S.L.], v. 312, p. 161-177, abr. 2015. Disponível em: https://www.sciencedirect.com/science/article/pii/S1571066115000146?via%3Dihub. Acesso em: 29 jul. 2020. http://dx.doi.org/10.1016/j.entcs.2015.04.010 1571-0661 https://repositorio.ufrn.br/jspui/handle/123456789/29761 10.1016/j.entcs.2015.04.010 en application/pdf Elsevier
institution Repositório Institucional
collection RI - UFRN
language English
topic Concurrent constraint programming
Temporal logic
Model checking
spellingShingle Concurrent constraint programming
Temporal logic
Model checking
Arias, Jaime
Guzman, Michell
Vega, Carlos Alberto Olarte
A Symbolic model for timed concurrent constraint programming
description 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
format article
author Arias, Jaime
Guzman, Michell
Vega, Carlos Alberto Olarte
author_facet Arias, Jaime
Guzman, Michell
Vega, Carlos Alberto Olarte
author_sort Arias, Jaime
title A Symbolic model for timed concurrent constraint programming
title_short A Symbolic model for timed concurrent constraint programming
title_full A Symbolic model for timed concurrent constraint programming
title_fullStr A Symbolic model for timed concurrent constraint programming
title_full_unstemmed A Symbolic model for timed concurrent constraint programming
title_sort symbolic model for timed concurrent constraint programming
publisher Elsevier
publishDate 2020
url https://repositorio.ufrn.br/jspui/handle/123456789/29761
work_keys_str_mv AT ariasjaime asymbolicmodelfortimedconcurrentconstraintprogramming
AT guzmanmichell asymbolicmodelfortimedconcurrentconstraintprogramming
AT vegacarlosalbertoolarte asymbolicmodelfortimedconcurrentconstraintprogramming
AT ariasjaime symbolicmodelfortimedconcurrentconstraintprogramming
AT guzmanmichell symbolicmodelfortimedconcurrentconstraintprogramming
AT vegacarlosalbertoolarte symbolicmodelfortimedconcurrentconstraintprogramming
_version_ 1773966060664389632

Registros relacionados