Operational and logical semantics for polling real-time systems

Henning Dierks; Ansgar Fehnker; Angelika H. Mader; Frits Vaandrager

doi:10.1007/BFb0055334

Operational and logical semantics for polling real-time systems

Henning Dierks
, Ansgar Fehnker
, Angelika H. Mader
, Frits Vaandrager

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

14 Citations (Scopus)

291 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Formal Techniques in Real-Time and Fault-Tolerant Systems
Subtitle of host publication	5th International Symposium, FTRTFT’98 Lyngby, Denmark, September 14–18, 1998 Proceedings
Editors	Anders P. Ravn, Hans Rischel
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	29-40
Number of pages	12
ISBN (Electronic)	978-3-540-49792-9
ISBN (Print)	978-3-540-65003-4
DOIs	https://doi.org/10.1007/BFb0055334
Publication status	Published - 1998
Event	5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 1998 - Lyngby, Denmark Duration: 14 Sept 1998 → 18 Sept 1998 Conference number: 5

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	1486
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 1998
Abbreviated title	FTRTFT
Country/Territory	Denmark
City	Lyngby
Period	14/09/98 → 18/09/98

Access to Document

10.1007/BFb0055334

Dierks1998operationalAccepted author version, 222 KB

Cite this

Dierks, H., Fehnker, A., Mader, A. H., & Vaandrager, F. (1998). Operational and logical semantics for polling real-time systems. In A. P. Ravn, & H. Rischel (Eds.), Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT’98 Lyngby, Denmark, September 14–18, 1998 Proceedings (pp. 29-40). (Lecture Notes in Computer Science; Vol. 1486). Springer. https://doi.org/10.1007/BFb0055334

Dierks, Henning ; Fehnker, Ansgar ; Mader, Angelika H. et al. / Operational and logical semantics for polling real-time systems. Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT’98 Lyngby, Denmark, September 14–18, 1998 Proceedings. editor / Anders P. Ravn ; Hans Rischel. Berlin, Heidelberg : Springer, 1998. pp. 29-40 (Lecture Notes in Computer Science).

@inproceedings{4fde28c8ab4147079e2dd96c261f3ba9,

title = "Operational and logical semantics for polling real-time systems",

abstract = "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.",

author = "Henning Dierks and Ansgar Fehnker and Mader, \{Angelika H.\} and Frits Vaandrager",

year = "1998",

doi = "10.1007/BFb0055334",

language = "English",

isbn = "978-3-540-65003-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "29--40",

editor = "Ravn, \{Anders P.\} and Hans Rischel",

booktitle = "Formal Techniques in Real-Time and Fault-Tolerant Systems",

address = "Germany",

note = "5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 1998, FTRTFT ; Conference date: 14-09-1998 Through 18-09-1998",

}

Dierks, H, Fehnker, A, Mader, AH & Vaandrager, F 1998, Operational and logical semantics for polling real-time systems. in AP Ravn & H Rischel (eds), Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT’98 Lyngby, Denmark, September 14–18, 1998 Proceedings. Lecture Notes in Computer Science, vol. 1486, Springer, Berlin, Heidelberg, pp. 29-40, 5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 1998, Lyngby, Denmark, 14/09/98. https://doi.org/10.1007/BFb0055334

Operational and logical semantics for polling real-time systems. / Dierks, Henning; Fehnker, Ansgar; Mader, Angelika H. et al.
Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT’98 Lyngby, Denmark, September 14–18, 1998 Proceedings. ed. / Anders P. Ravn; Hans Rischel. Berlin, Heidelberg: Springer, 1998. p. 29-40 (Lecture Notes in Computer Science; Vol. 1486).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Dierks, Henning

AU - Fehnker, Ansgar

AU - Mader, Angelika H.

AU - Vaandrager, Frits

N1 - Conference code: 5

PY - 1998

Y1 - 1998

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.

U2 - 10.1007/BFb0055334

DO - 10.1007/BFb0055334

M3 - Conference contribution

SN - 978-3-540-65003-4

T3 - Lecture Notes in Computer Science

SP - 29

EP - 40

BT - Formal Techniques in Real-Time and Fault-Tolerant Systems

A2 - Ravn, Anders P.

A2 - Rischel, Hans

PB - Springer

CY - Berlin, Heidelberg

T2 - 5th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems, FTRTFT 1998

Y2 - 14 September 1998 through 18 September 1998

ER -

Dierks H, Fehnker A, Mader AH, Vaandrager F. Operational and logical semantics for polling real-time systems. In Ravn AP, Rischel H, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems: 5th International Symposium, FTRTFT’98 Lyngby, Denmark, September 14–18, 1998 Proceedings. Berlin, Heidelberg: Springer. 1998. p. 29-40. (Lecture Notes in Computer Science). doi: 10.1007/BFb0055334

Operational and logical semantics for polling real-time systems

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this