Sciweavers

Share
FTRTFT
1998
Springer

Operational and Logical Semantics for Polling Real-Time Systems

10 years 4 days ago
Operational and Logical Semantics for Polling Real-Time Systems
PLC-Automata are a class of real-time automata suitable to describe the behavior of polling real-time systems. PLC-Automata can be compiled to source code for PLCs, a hardware widely used in industry to control processes. Also, PLC-Automata have been equipped with a logical and operational semantics, using Duration Calculus (DC) and Timed Automata (TA), respectively. The three main results of this paper are: (1) A simpli ed operational semantics. (2) A minor extension of the logical semantics, and a proof that this semantics is complete relative to our operational semantics. This means that if an observable satis es all formulas of the DC semantics, then it can also be generated by the TA semantics. (3) A proof that the logical semantics is sound relative to our operational semantics. This means that each observable that is accepted by the TA semantics constitutes a model for all formulas of the DC semantics.
Henning Dierks, Ansgar Fehnker, Angelika Mader, Fr
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where FTRTFT
Authors Henning Dierks, Ansgar Fehnker, Angelika Mader, Frits W. Vaandrager
Comments (0)
books