Related papers: Modal Specifications for Probabilistic Timed Syste…
The complexity of modern software systems entails the need for reconfiguration mechanisms gov- erning the dynamic evolution of their execution configurations in response to both external stimulus or internal performance measures. Formally,…
Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise. During the past 25+ years, team automata have been studied and…
Modular and reconfigurable robotic systems have been designed to provide a customized solution for the non-repetitive tasks to be performed in a constrained environment. Customized solutions are normally extracted from task-based…
Timed automata are the formal model for real-time systems. Extensions with discrete probabilistic branching have been considered in the literature and successfully applied. Probabilistic timed automata (PTA) do require all branching…
In this paper we introduce a framework for option model composition. Option models are temporal abstractions that, like macro-operators in classical planning, jump directly from a start state to an end state. Prior work has focused on…
Suitable extensions of the monadic second-order theory of k successors have been proposed in the literature to capture the notion of time granularity. In this paper, we provide the monadic second-order theories of downward unbounded layered…
An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that…
The predominant knowledge-based approach to automated model construction, compositional modelling, employs a set of models of particular functional components. Its inference mechanism takes a scenario describing the constituent interacting…
We present abstraction-refinement algorithms for model checking safety properties of timed automata. The abstraction domain we consider abstracts away zones by restricting the set of clock constraints that can be used to define them, while…
Simulation-based compositional abstraction effectively mitigates state space explosion in model checking, particularly for timed systems. However, existing approaches do not support broadcast synchronization, an important mechanism for…
Bisimulation metric is a robust behavioural semantics for probabilistic processes. Given any SOS specification of probabilistic processes, we provide a method to compute for each operator of the language its respective metric…
In this paper, we focus on the design and verification of timed automata (TA). We introduce a new method for assisting construction and verification of TA models along with a tool implementing the proposed method, i.e., ATAC: Automated…
This paper establishes relative expressiveness results for several modal mu-calculi interpreted over timed automata. These mu-calculi combine modalities for expressing passage of (real) time with a general framework for defining formulas…
We discuss various formalisms to describe string-to-string transformations. Many are based on automata and can be seen as operational descriptions, allowing direct implementations when the input scanner is deterministic. Alternatively, one…
We present a framework to formally describe probabilistic system behavior and symbolically reason about it. In particular we aim at reasoning about possible failures and fault tolerance. We regard systems which are composed of different…
We consider previous models of Timed, Probabilistic and Stochastic Timed Automata, we introduce our model of Timed Automata with Polynomial Delay and we characterize the expressiveness of these models relative to each other.
A formal description of a Cyber-Physical system should include a rigorous specification of the computational and physical components involved, as well as their interaction. Such a description, thus, lends itself to a compositional model…
Imprecise probability is concerned with uncertainty about which probability distributions to use. It has applications in robust statistics and machine learning. We look at programming language models for imprecise probability. Our…
This paper introduces operators, semantics, characterizations, and solution-independent conditions to guarantee temporal logic specifications for hybrid dynamical systems. Hybrid dynamical systems are given in terms of differential…
We explore different ways of implementing temporal constraints expressed in an extension of Answer Set Programming (ASP) with language constructs from dynamic logic. Foremost, we investigate how automata can be used for enforcing such…