Extending Timed Automaton and Real-Time Logic to Many-Valued Reasoning

  • Ana Fernández Vilas
  • José J. Pazos Arias
  • Rebeca P. Díaz Redondo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


Past decade has witnessed a great advance in the field of dense-time formal methods for the specification, synthesis and analysis of real time systems. In this context timed automata and real-time temporal logics provide a simple, and yet general, way to model and specify the behavior of these systems. At the same time, iterative and incremental development has been massively adopted in professional practice. In order to get closer to this current trend, timed formal methods should be adapted to such lifecycle structures, getting over their traditional role of verifying that a model meets a set of fixed requirements. We advocate the suitability of many-valued reasoning in order to achieve this goal; in the scope of knowledge representation, many-valued reasoning is suitable to deal with both uncertainty and disagreement which are pervasive and desirable in an iterative and incremental design process. In this respect, this paper introduces SCTL/MUS-T methodology as an extension of timed automata and temporal logic theories to many-valued reasoning in real-time.


Model Check Temporal Logic Discrete Transition Time Automaton Predicate Transformer 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Alur, R.: Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Department of Computer Science, Stanford University (1991)Google Scholar
  2. 2.
    Gollu, A., Puri, A., Varaiya, P.: Discretization of Timed Automata. In: Decision and Control, 33rd IEEE Conference. (1994) 957–958Google Scholar
  3. 3.
    Asarin, E., Maler, O., Pnueli, A.: On Discretization of Delays in Timed Automata and Digital Circuits. In: Concurrency Theory, 9th International Conference (CON-CUR’98). Volume 1466 of LNCS. Springer Verlag (1998) 470–484Google Scholar
  4. 4.
    Alur, R., Henzinger, T.A.: Logics and Models of Real Time: A Survey. In: Real Time: Theory and Practice, REX Workshop. Volume 600 of LNCS. Springer Verlag (1992) 74–106CrossRefGoogle Scholar
  5. 5.
    Alur, R., Courcoubetis, C., Dill, D.: Model Checking in Dense Real-time. Information and Computation 104 (1993) 2–34zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Chechik, M., Devereux, B., Easterbrook, S.M., Lai, A., Petrovykh, V.: Efficient Multiple-Valued Model-Checking Using Lattice Representations. In: Concurrency Theory, 12th International Conference (CONCUR’01). (2001) 21–24Google Scholar
  7. 7.
    Pazos Arias, J.J., García Duque, J.: SCTL-MUS: A Formal Methodology for Software Development of Distributed Systems. A Case Study. Formal Aspects of Computing 13 (2001) 50–91zbMATHCrossRefGoogle Scholar
  8. 8.
    Fernández Vilas, A.: Tratamiento Formal de Sistemas con Requisitos de Tiempo Real Críticos. PhD thesis, Dept. Ingeniería Telemática, Universidad de Vigo (2002)Google Scholar
  9. 9.
    Sokolsky, O.V., Smolka, S.A.: Local Model Checking for Real-Time Systems. In: Computer Aided Verification, 7th International Conference (CAV’95). Volume 939 of LNCS., Springer Verlag (1995) 211–224Google Scholar
  10. 10.
    Tarski, A.: A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics 5 (1955) 285–309zbMATHMathSciNetGoogle Scholar
  11. 11.
    Barringer, H., Fisher, M., Gabbay, D., Gough, G., Owens, R.: METATEM: An Introduction. Formal Aspects of Computing 7 (1995) 533–549zbMATHCrossRefGoogle Scholar
  12. 12.
    Laroussinie, F., Larsen, K.G., Weise, C.: From Timed Automata to Logic-And Back. In: Mathematical Foundations of Computer Science, 20th International Symposium (MFCS’95). Volume 969 of LNCS., Springer Verlag (1995) 529–539Google Scholar
  13. 13.
    Wong Toi, H., Hoffmann, G.: The Control of Dense Real Time Discrete Event Systems. In: Decision and Control, 30th IEEE Conference. (1991) 1527–1528Google Scholar
  14. 14.
    Alur, R., Courcoubetis, C., Halbwachs, N., Dill, D.L., Wong Toi, H.: Minimization of Timed Transition Systems. In: Concurrency Theory, 3rd International Conference (CONCUR’92). Volume 630 of LNCS., Spinger Verlag (1992) 340–354Google Scholar
  15. 15.
    Abrial, J.R., Borger, E., Langmaack, H.: Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control. Volume 1165 of LNCS. Springer Verlag (1996)Google Scholar
  16. 16.
    Cerans, K., Godskesen, J.C., Larsen, K.G.: Timed Modal Specifications-Theory and Tools. In: Computer Aided Verification, 5th International Conference (CAV’93). Volume 697 of LNCS., Springer Verlag (1993) 253–267Google Scholar
  17. 17.
    García Duque, J., Pazos Arias, J.J.: Reasoning over Inconsistent Viewpoints: How levels of agreement can evolve? In: Living With Inconsistency, 2nd International Workshop (ICSE’01). (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Ana Fernández Vilas
    • 1
  • José J. Pazos Arias
    • 1
  • Rebeca P. Díaz Redondo
    • 1
  1. 1.Departamento de Ingeniería TelemáticaUniversidad de VigoVigoSpain

Personalised recommendations