Stochastic Concurrency in Rewrite-Based Probabilistic Models (SCORES).

Many systems are probabilistic in nature because the occurrence of events cannot be perfectly predicted. This behavior can be due to the uncertainty of the environment in which these systems must operate or to the probabilistic nature intrinsic to its dynamics, or to both. Reactive systems are a broad class of real-time concurrent systems in which both probabilistic and non-deterministic aspects may coexist: different transitions may be triggered concurrently, and the outcome of some of them may be probabilistic. The reason why reactive systems are of particular interest is that they can illustrate the complexity and nature of today's ubiquitous computing where many agents execute and share information in a distributed configuration. However, providing executable specifications to reactive computation is a significant challenge since traditional mathematical models of computation do not provide off-the-shelf techniques and tools to reason about important aspects of these systems. This project takes up the task of developing an executable semantics for the precise specification of probabilistic behavior (i.e., behavior resulting from probabilistic choice) in reactive systems, where both internal and external non-determinism play a central role. More precisely, the main goal of this proposal is to develop computational techniques and tools for reactive systems that will enable the quantitative analysis of properties for PNTCC. The main challenge is that concurrent systems in this setting can exhibit any combination of probabilistic choice and flow of private and public information. In the end, the state of the art will be advanced in different domains including probabilistic concurrent systems, probabilistic rewriting logic specification, and automated analysis. This may enable a systematic and automatic approach to the analysis of quantitative aspects of today's reactive and ubiquitous systems such as cloud-based computation, social networking, and mission-critical applications.