On the Verification of Nondeterministic Automata Specifications of Probabilistic Real-Time Systems

Abstract: Alur et al.~presented an algorithm for the problem of verifying deterministic timed automata specifications of probabilistic real-time systems given as generalized semi-Markov processes; and posed the question of the verification of nondeterministic specifications. We give a partial answer to the question, extending their method so that processes, with a fairly acceptable restriction, can be tested against any timed automaton. These include, for instance, real-time models of digital circuits where the key property is that the delay distributions have non-zero lower bounds.



Resumo: Alur et al.~apresentaram um algoritmo para o problema de verificação de processos de tempo real probabilísticos contra especificações dadas por autômatos temporais; e levantaram a questão da verificação de especificações dadas por autômatos não determinísticos. Nesse artigo, nós damos uma resposta parcial para a questão, extendendo o método de tal forma que processos, com uma restrição aceitável, podem ser testados contra qualquer autômato temporal. Entre esses processos, por exemplo, incluem-se modelos de circuitos digitais onde a propriedade principal é que as distribuições dos atrasos possuem limite inferior diferente de zero.

1999