TY - GEN
T1 - Real-time rewriting logic semantics for spatial concurrent constraint programming
AU - Ramírez, Sergio
AU - Romero, Miguel
AU - Rocha, Camilo
AU - Valencia, Frank
N1 - Publisher Copyright:
© Springer Nature Switzerland AG 2018.
PY - 2018/1/1
Y1 - 2018/1/1
N2 - Process calculi provide a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. This paper uses rewriting logic for specifying and analyzing a process calculus for concurrent constraint programming (ccp), combining spatial and real-time behavior. In these systems, agents can run processes in different computational spaces (e.g., containers) while subject to real-time requirements (e.g., upper bounds in the execution time of a given operation), which can be specified with both discrete and dense linear time. The real-time rewriting logic semantics is fully executable in Maude with the help of rewriting modulo SMT: partial information (i.e., constraints) in the specification is represented by quantifier-free formulas on the shared variables of the system that are under the control of SMT decision procedures. The approach is used to symbolically analyze existential real-time reachability properties of process calculi in the presence of spatial hierarchies for sharing information and knowledge.
AB - Process calculi provide a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. This paper uses rewriting logic for specifying and analyzing a process calculus for concurrent constraint programming (ccp), combining spatial and real-time behavior. In these systems, agents can run processes in different computational spaces (e.g., containers) while subject to real-time requirements (e.g., upper bounds in the execution time of a given operation), which can be specified with both discrete and dense linear time. The real-time rewriting logic semantics is fully executable in Maude with the help of rewriting modulo SMT: partial information (i.e., constraints) in the specification is represented by quantifier-free formulas on the shared variables of the system that are under the control of SMT decision procedures. The approach is used to symbolically analyze existential real-time reachability properties of process calculi in the presence of spatial hierarchies for sharing information and knowledge.
U2 - 10.1007/978-3-319-99840-4_13
DO - 10.1007/978-3-319-99840-4_13
M3 - Conference contribution
AN - SCOPUS:85053892233
SN - 9783319998398
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 226
EP - 244
BT - Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, 2018, Proceedings
A2 - Rusu, Vlad
PB - Springer Verlag
T2 - 12th International Workshop on Rewriting Logic and its Applications, WRLA 2018
Y2 - 14 June 2018 through 15 June 2018
ER -