Real-Time Rewriting Logic Semantics For Spatial Concurrent Constraint Programming

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.