From timed automata to stochastic hybrid games model checking, synthesis, performance analysis and machine learning

Kim G. Larsen; Uli Fahrenberg; Axel Legay

doi:10.3233/978-1-61499-810-5-60

From timed automata to stochastic hybrid games model checking, synthesis, performance analysis and machine learning

Kim G. Larsen^*, Uli Fahrenberg, Axel Legay

^*Corresponding author for this work

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

1 Citation (Scopus)

Abstract

This article aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the timed automata modeling formalism introduced by Alur and Dill [8,9]. The paper gives comprehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on associated decision problems related to model checking, equivalence checking, optimal scheduling, the existence of winning strategies. Also the article provides the stochastic semantic extension of timed automata and timed games enabling statistical model checking as well as optimal synthesis using reinforcement learning.

Original language	English
Title of host publication	Dependable Software Systems Engineering
Number of pages	44
Publisher	IOS Press
Publication date	1 Jan 2017
Pages	60-103
ISBN (Print)	9781614998099
ISBN (Electronic)	9781614998105
DOIs	https://doi.org/10.3233/978-1-61499-810-5-60
Publication status	Published - 1 Jan 2017

Bibliographical note

Publisher Copyright:
© 2017 The authors and IOS Press. All rights reserved.

Copyright:
Copyright 2018 Elsevier B.V., All rights reserved.

Keywords

Bisimilarity
Conditional optimality
Optimal infinite run
Optimal reachability
Optimal winning strategies
Priced timed automaton
Reachability
Region
Statistical model checking
Stochastic timed automata
Stochastic timed games
Timed automaton
Timed game
Weighted timed automaton
Winning strategy
Zone

Access to Document

10.3233/978-1-61499-810-5-60

AUB Link

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

Cite this

@inbook{d46120efedf7442eb1a1cf0dd34d19cb,

title = "From timed automata to stochastic hybrid games model checking, synthesis, performance analysis and machine learning",

abstract = "This article aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the timed automata modeling formalism introduced by Alur and Dill [8,9]. The paper gives comprehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on associated decision problems related to model checking, equivalence checking, optimal scheduling, the existence of winning strategies. Also the article provides the stochastic semantic extension of timed automata and timed games enabling statistical model checking as well as optimal synthesis using reinforcement learning.",

keywords = "Bisimilarity, Conditional optimality, Optimal infinite run, Optimal reachability, Optimal winning strategies, Priced timed automaton, Reachability, Region, Statistical model checking, Stochastic timed automata, Stochastic timed games, Timed automaton, Timed game, Weighted timed automaton, Winning strategy, Zone",

author = "Larsen, {Kim G.} and Uli Fahrenberg and Axel Legay",

year = "2017",

month = jan,

day = "1",

doi = "10.3233/978-1-61499-810-5-60",

language = "English",

isbn = "9781614998099",

pages = "60--103",

booktitle = "Dependable Software Systems Engineering",

publisher = "IOS Press",

address = "Netherlands",

}

TY - CHAP

T1 - From timed automata to stochastic hybrid games model checking, synthesis, performance analysis and machine learning

AU - Larsen, Kim G.

AU - Fahrenberg, Uli

AU - Legay, Axel

PY - 2017/1/1

Y1 - 2017/1/1

N2 - This article aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the timed automata modeling formalism introduced by Alur and Dill [8,9]. The paper gives comprehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on associated decision problems related to model checking, equivalence checking, optimal scheduling, the existence of winning strategies. Also the article provides the stochastic semantic extension of timed automata and timed games enabling statistical model checking as well as optimal synthesis using reinforcement learning.

AB - This article aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the timed automata modeling formalism introduced by Alur and Dill [8,9]. The paper gives comprehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on associated decision problems related to model checking, equivalence checking, optimal scheduling, the existence of winning strategies. Also the article provides the stochastic semantic extension of timed automata and timed games enabling statistical model checking as well as optimal synthesis using reinforcement learning.

KW - Bisimilarity

KW - Conditional optimality

KW - Optimal infinite run

KW - Optimal reachability

KW - Optimal winning strategies

KW - Priced timed automaton

KW - Reachability

KW - Region

KW - Statistical model checking

KW - Stochastic timed automata

KW - Stochastic timed games

KW - Timed automaton

KW - Timed game

KW - Weighted timed automaton

KW - Winning strategy

KW - Zone

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

U2 - 10.3233/978-1-61499-810-5-60

DO - 10.3233/978-1-61499-810-5-60

M3 - Book chapter

AN - SCOPUS:85046427422

SN - 9781614998099

SP - 60

EP - 103

BT - Dependable Software Systems Engineering

PB - IOS Press

ER -

From timed automata to stochastic hybrid games model checking, synthesis, performance analysis and machine learning

Abstract

Bibliographical note

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

Cite this