### Abstract

Original language | Undefined |
---|---|

Pages | 29-40 |

Number of pages | 12 |

DOIs | |

Publication status | Published - Sep 1998 |

### Keywords

- IR-56216
- EWI-1051

### Cite this

*Operational and logical semantics for polling real-time systems*. 29-40. https://doi.org/10.1007/BFb0055334

}

**Operational and logical semantics for polling real-time systems.** / Anders, P.R. (Editor); Dierks, Henning; Fehnker, Ansgar; Rischel, H. (Editor); Fehnker, Ansgar; Mader, Angelika H.; Vaandrager, Frits.

Research output: Contribution to conference › Paper › Academic › peer-review

TY - CONF

T1 - Operational and logical semantics for polling real-time systems

AU - Dierks, Henning

AU - Fehnker, Ansgar

AU - Fehnker, Ansgar

AU - Mader, Angelika H.

AU - Vaandrager, Frits

A2 - Anders, P.R.

A2 - Rischel, H.

N1 - Imported from DIES

PY - 1998/9

Y1 - 1998/9

N2 - 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 simplified 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 satisfies 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.

AB - 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 simplified 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 satisfies 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.

KW - IR-56216

KW - EWI-1051

U2 - 10.1007/BFb0055334

DO - 10.1007/BFb0055334

M3 - Paper

SP - 29

EP - 40

ER -