Title
Modal Specifications For Probabilistic Timed Systems
Abstract
Modal automata are a classic formal model for component-based systems that comes equipped with a rich specification theory supporting abstraction, refinement and compositional reasoning. In recent years, quantitative variants of modal automata were introduced for specifying and reasoning about component-based designs for embedded and mobile systems. These respectively generalize modal specification theories for timed and probabilistic systems. In this paper, we define a modal specification language for combined probabilistic timed systems, called abstract probabilistic timed automata, which generalizes existing formalisms. We introduce appropriate syntactic and semantic refinement notions and discuss consistency of our specification language, also with respect to timedivergence. We identify a subclass of our models for which we define the fundamental operations for abstraction, conjunction and parallel composition, and show several compositionality results.
Year
DOI
Venue
2013
10.4204/EPTCS.117.5
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE
Field
DocType
Issue
Specification language,Abstraction,Computer science,Automaton,Theoretical computer science,Compositional reasoning,Probabilistic logic,Syntax,Rotation formalisms in three dimensions,Modal
Journal
117
ISSN
Citations 
PageRank 
2075-2180
0
0.34
References 
Authors
15
4
Name
Order
Citations
PageRank
Tingting Han124819.06
Christian Krause225412.93
Marta Z. Kwiatkowska36118322.21
Holger Giese42345164.90