Projects per year
Abstract
In this paper we develop and study the Recursive Weighted Logic (RWL), a multi-modal logic that expresses qualitative and quantitative properties of labelled weighted transition systems (LWSs). LWSs are transition systems labelled with actions and real-valued quantities representing the costs of transitions with respect to various resources. RWL uses first-order variables to measure local costs. The main syntactic operators are similar to the ones of timed logics for real-time systems. In addition, our logic is endowed, with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We prove that unlike in the case of the timed logics, the satisfiability problem for RWL is decidable. The proof uses a variant of the region construction technique used in literature with timed automata, which we adapt to the specific settings of RWL. This paper extends previous results that we have demonstrated for a similar but much more restrictive logic that can only use one variable for each type of resource to encode logical properties.
Original language | English |
---|---|
Title of host publication | Theoretical Aspects of Computing – ICTAC 2014 : 11th International Colloquium, Bucharest, Romania, September 17-19, 2014. Proceedings |
Editors | Gabriel Ciobanu, Dominique Méry |
Number of pages | 17 |
Volume | 8687 |
Publisher | Springer Publishing Company |
Publication date | 2014 |
Pages | 460-476 |
ISBN (Print) | 978-3-319-10881-0 |
ISBN (Electronic) | 978-3-319-10882-7 |
DOIs | |
Publication status | Published - 2014 |
Event | 11th International Colloquium on Theoretical Aspects of Computing - Central University Library of Bucharest, Bucharest, Romania Duration: 17 Sept 2014 → 19 Sept 2014 Conference number: 11 |
Conference
Conference | 11th International Colloquium on Theoretical Aspects of Computing |
---|---|
Number | 11 |
Location | Central University Library of Bucharest |
Country/Territory | Romania |
City | Bucharest |
Period | 17/09/2014 → 19/09/2014 |
Series | Lecture Notes in Computer Science |
---|---|
ISSN | 0302-9743 |
Keywords
- labelled weighted transition system
- multi-modal logic
- maximal fixed point computation
Fingerprint
Dive into the research topics of 'A Decidable Recursive Logic for Weighted Transition Systems'. Together they form a unique fingerprint.Projects
- 1 Finished
-
IDEA4CPS: Foundations for Cyber-Physical Sytems
Larsen, K. G., Skou, A., Nielsen, B., Bulychev, P., Ravn, A. P. & Poulsen, D. B.
01/04/2011 → 30/04/2015
Project: Research