@techreport{TR-IC-99-27,
  number = {IC-99-27},
  author = {Arnaldo V. Moura and Guilherme A. Pinto},
  title = {On the Verification of Nondeterministic Automata Specifications of Probabilistic Real-Time Systems},
  month = {December},
  year = {1999}, 
  institution = {Institute of Computing, University of Campinas},
  note = {In English, 24 pages.
    \par\selectlanguage{brazil}\textbf{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.
    
    \par\selectlanguage{english}\textbf{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.
  }
}