跳到主要导航 跳到搜索 跳到主要内容

A proof system for timed automata

  • Chinese Academy of Sciences
  • Uppsala University

科研成果: 书/报告/会议事项章节会议稿件同行评审

摘要

A proof system for timed automata is presented, based on a CCS-style language for describing timed automata. It consists of the standard monoid laws for bisimulation and a set of inference rules. The judgments of the proof system are conditional equations of the form θ ▷ t = u where θ is a clock constraint and t, u are terms denoting timed automata. It is proved that the proof system is complete for timed bisimulation over the recursion-free subset of the language. The completeness proof relies on the notion of symbolic timed bisimulation. The axiomatisation is also extended to handle an important variation of timed automata where each node is associated with an invariant constraint.

源语言英语
主期刊名Foundations of Software Science and Computation Structures - Third International Conference, FOSSACS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000
编辑Jerzy Tiuryn
出版商Springer Verlag
208-222
页数15
ISBN(印刷版)3540672575, 9783540672579
DOI
出版状态已出版 - 2000
已对外发布
活动3rd International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000 - Berlin, 德国
期限: 25 3月 20002 4月 2000

出版系列

姓名Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
1784 LNCS
ISSN(印刷版)0302-9743
ISSN(电子版)1611-3349

会议

会议3rd International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2000, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2000
国家/地区德国
Berlin
时期25/03/002/04/00

学术指纹

探究 'A proof system for timed automata' 的科研主题。它们共同构成独一无二的学术指纹。

引用此