Dual-priced modal transition systems with time durations

Nikola Beneš, Jan Křetínský, Kim Guldstrand Larsen, Mikael H. Møller, Jiří Srba

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

11 Scopus citations

Abstract

Modal transition systems are a well-established specification formalism for a high-level modelling of component-based software systems. We present a novel extension of the formalism called modal transition systems with durations where time durations are modelled as controllable or uncontrollable intervals. We further equip the model with two kinds of quantitative aspects: each action has its own running cost per time unit, and actions may require several hardware components of different costs. We ask the question, given a fixed budget for the hardware components, what is the implementation with the cheapest long-run average reward. We give an algorithm for computing such optimal implementations via a reduction to a new extension of mean payoff games with time durations and analyse the complexity of the algorithm.

Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Proceedings
Pages122-137
Number of pages16
DOIs
StatePublished - 2012
Event18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18 - Merida, Venezuela, Bolivarian Republic of
Duration: 11 Mar 201215 Mar 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7180 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18
Country/TerritoryVenezuela, Bolivarian Republic of
CityMerida
Period11/03/1215/03/12

Fingerprint

Dive into the research topics of 'Dual-priced modal transition systems with time durations'. Together they form a unique fingerprint.

Cite this