Towards a correct and efficient implementation of simulation and verification tools for probabilistic ntcc

TL;DR

This paper extends a simulation tool for probabilistic ntcc models and introduces a verification tool capable of proving probabilistic properties, aiming to improve correctness and efficiency in modeling complex systems.

Contribution

The paper presents new extensions to simulation and verification tools for probabilistic ntcc, enabling probabilistic property verification and addressing current limitations.

Findings

Successfully extended simulation tool Ntccrt for pntcc models

Developed a verification tool for probabilistic properties

Identified current limitations and future development plans

Abstract

We extended our simulation tool Ntccrt for probabilistic ntcc (pntcc) models. In addition, we developed a verification tool for pntcc models. Using this tool we can prove properties such as the system will go to a successful state with probability p under t discrete time- units. Currently, we are facing a few problems. We can only verify pntcc models using a finite domain constraint system and the encoding of cells ( mathematical entities that can update their value ) is experimental. In addition, in order to reduce the states generated during the verification process we need to implement a procedure to calculate whether two processes are equivalent. In the future, we want to provide multiple interfaces for the tools (e.g., a web ap- plication, a graphical interface and command line interface). We also want to support constraint systems over trees, graph and sets. We want to show the relevance of our tool to model biological and multimedia interaction systems in our tool, verify some properties about them, and simulate such systems in our real-time capable interpreter.