SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Results on Event-Recording Logic
 by Maria Sorea.

We present construction of characteristic formulas for event-recording automata in terms of the ERLv logic, a real-time extension of the Hennessy-Milner Logic with greatest fixpoints. By combining the construction of characteristic formulas with the model checking algorithm for ERLv, we obtain a decision procedure for timed bisimilarity and timed similarity for event-recording automata. Furthermore, we present decidability results for the fixpoint free fragment of ERLv, denoted by ERL. We show that the model checking problem for event-recording automata and ERL is PSPACE-complete, and that the satisfiability problem for ERL is decidable. 'We present a tableau-based decision procedure that allows the decision of whether or not a given ERL formula is valid. We introduce a set of reduction rules for constructing tableaux for ERL formulas, and show that these rules form a sound and complete tableau system.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2019 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy