New Results on Timed Specifications

Timothy Bourke; Alexandre David; Kim Guldstrand Larsen; Axel Legay; Didier Lime; Ulrik Nyman; Andrzej Wasowski

doi:10.1007/978-3-642-28412-0_12

New Results on Timed Specifications

Timothy Bourke, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Didier Lime, Ulrik Nyman, Andrzej Wasowski

Research output: Contribution to book/anthology/report/conference proceeding › Book chapter › Research › peer-review

4 Citations (Scopus)

511 Downloads (Pure)

Abstract

Recently, we have proposed a new design theory for timed systems.
This theory, building on Timed I/O Automata with game semantics, includes clas-
sical operators like satisfaction, consistency, logical composition and structural
composition. This paper presents a new efficient algorithm for checking Büchi
objectives of timed games. This new algorithm can be used to strengthen the in-
finite behavior of an interface, or to guarantee that the interface can indeed be
implemented. We illustrate the framework with an infrared sensor case study.

Original language	English
Title of host publication	Recent Trends in Algebraic Development Techniques : 20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers
Editors	Till Mossakowski, Hans-Jörg Kreowski
Number of pages	18
Publisher	Springer
Publication date	23 Feb 2012
Pages	175-192
ISBN (Print)	978-3-642-28411-3
ISBN (Electronic)	978-3-642-28412-0
DOIs	https://doi.org/10.1007/978-3-642-28412-0_12
Publication status	Published - 23 Feb 2012
Event	20th International Workshop on Algebraic Development Techniques WADT 2010 - Duration: 1 Jul 2010 → 4 Jul 2010

Conference

Conference	20th International Workshop on Algebraic Development Techniques WADT 2010
Period	01/07/2010 → 04/07/2010

Series	Lecture Notes in Computer Science
Volume	7137
ISSN	0302-9743

Access to Document

10.1007/978-3-642-28412-0_12

WADT2010.pdfAccepted author manuscript, 184 KB

AUB Link

Search for the material in Aalborg University Library's search engine

Cite this

Bourke, T., David, A., Larsen, K. G., Legay, A., Lime, D., Nyman, U., & Wasowski, A. (2012). New Results on Timed Specifications. In T. Mossakowski, & H-J. Kreowski (Eds.), Recent Trends in Algebraic Development Techniques: 20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers (pp. 175-192). Springer. https://doi.org/10.1007/978-3-642-28412-0_12

Bourke, Timothy ; David, Alexandre ; Larsen, Kim Guldstrand et al. / New Results on Timed Specifications. Recent Trends in Algebraic Development Techniques: 20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers. editor / Till Mossakowski ; Hans-Jörg Kreowski. Springer, 2012. pp. 175-192 (Lecture Notes in Computer Science, Vol. 7137).

@inbook{ca334eadb4fd417e9aeb08e20e7bda66,

title = "New Results on Timed Specifications",

abstract = "Recently, we have proposed a new design theory for timed systems.This theory, building on Timed I/O Automata with game semantics, includes clas-sical operators like satisfaction, consistency, logical composition and structuralcomposition. This paper presents a new efficient algorithm for checking B{\"u}chiobjectives of timed games. This new algorithm can be used to strengthen the in-finite behavior of an interface, or to guarantee that the interface can indeed beimplemented. We illustrate the framework with an infrared sensor case study.",

author = "Timothy Bourke and Alexandre David and Larsen, {Kim Guldstrand} and Axel Legay and Didier Lime and Ulrik Nyman and Andrzej Wasowski",

year = "2012",

month = feb,

day = "23",

doi = "10.1007/978-3-642-28412-0_12",

language = "English",

isbn = "978-3-642-28411-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "175--192",

editor = "Till Mossakowski and Hans-J{\"o}rg Kreowski",

booktitle = "Recent Trends in Algebraic Development Techniques",

address = "Germany",

note = "20th International Workshop on Algebraic Development Techniques WADT 2010 ; Conference date: 01-07-2010 Through 04-07-2010",

}

Bourke, T, David, A, Larsen, KG, Legay, A, Lime, D, Nyman, U & Wasowski, A 2012, New Results on Timed Specifications. in T Mossakowski & H-J Kreowski (eds), Recent Trends in Algebraic Development Techniques: 20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers. Springer, Lecture Notes in Computer Science, vol. 7137, pp. 175-192, 20th International Workshop on Algebraic Development Techniques WADT 2010, 01/07/2010. https://doi.org/10.1007/978-3-642-28412-0_12

New Results on Timed Specifications. / Bourke, Timothy; David, Alexandre; Larsen, Kim Guldstrand et al.
Recent Trends in Algebraic Development Techniques: 20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers. ed. / Till Mossakowski; Hans-Jörg Kreowski. Springer, 2012. p. 175-192 (Lecture Notes in Computer Science, Vol. 7137).

Research output: Contribution to book/anthology/report/conference proceeding › Book chapter › Research › peer-review

TY - CHAP

T1 - New Results on Timed Specifications

AU - Bourke, Timothy

AU - David, Alexandre

AU - Larsen, Kim Guldstrand

AU - Legay, Axel

AU - Lime, Didier

AU - Nyman, Ulrik

AU - Wasowski, Andrzej

PY - 2012/2/23

Y1 - 2012/2/23

N2 - Recently, we have proposed a new design theory for timed systems.This theory, building on Timed I/O Automata with game semantics, includes clas-sical operators like satisfaction, consistency, logical composition and structuralcomposition. This paper presents a new efficient algorithm for checking Büchiobjectives of timed games. This new algorithm can be used to strengthen the in-finite behavior of an interface, or to guarantee that the interface can indeed beimplemented. We illustrate the framework with an infrared sensor case study.

AB - Recently, we have proposed a new design theory for timed systems.This theory, building on Timed I/O Automata with game semantics, includes clas-sical operators like satisfaction, consistency, logical composition and structuralcomposition. This paper presents a new efficient algorithm for checking Büchiobjectives of timed games. This new algorithm can be used to strengthen the in-finite behavior of an interface, or to guarantee that the interface can indeed beimplemented. We illustrate the framework with an infrared sensor case study.

UR - http://www.scopus.com/inward/record.url?scp=84857740549&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-28412-0_12

DO - 10.1007/978-3-642-28412-0_12

M3 - Book chapter

SN - 978-3-642-28411-3

T3 - Lecture Notes in Computer Science

SP - 175

EP - 192

BT - Recent Trends in Algebraic Development Techniques

A2 - Mossakowski, Till

A2 - Kreowski, Hans-Jörg

PB - Springer

T2 - 20th International Workshop on Algebraic Development Techniques WADT 2010

Y2 - 1 July 2010 through 4 July 2010

ER -

Bourke T, David A, Larsen KG, Legay A, Lime D, Nyman U et al. New Results on Timed Specifications. In Mossakowski T, Kreowski H-J, editors, Recent Trends in Algebraic Development Techniques: 20th International Workshop, WADT 2010, Etelsen, Germany, July 1-4, 2010, Revised Selected Papers. Springer. 2012. p. 175-192. (Lecture Notes in Computer Science, Vol. 7137). doi: 10.1007/978-3-642-28412-0_12

New Results on Timed Specifications

Abstract

Conference

Access to Document

AUB Link

Other files and links

Cite this