|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'501'711
Articles rated: 2609
19 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
Parameterized Linear Temporal Logics Meet Costs: Still not Costlier than LTL | | Martin Zimmermann
; | | Date: |
24 Sep 2015 | | Abstract: | We continue the investigation of parameterized extensions of Linear Temporal
Logic (LTL) that retain the attractive algorithmic properties of LTL: a
polynomial space model checking algorithm and a doubly-exponential time
algorithm for solving games. Alur et al. and Kupferman et al. showed that this
is the case for Parametric LTL (PLTL) and PROMPT-LTL respectively, which have
temporal operators equipped with variables that bound their scope in time.
Later, this was also shown to be true for Parametric LDL (PLDL), which extends
PLTL to be able to express all omega-regular properties.
Here, we generalize PLTL to systems with costs, i.e., we do not bound the
scope of operators in time, but bound the scope in terms of the cost
accumulated during time. Again, we show that model checking and solving games
for specifications in PLTL with costs is not harder than the corresponding
problems for LTL. Finally, we discuss PLDL with costs and extensions to
multiple cost functions. | | Source: | arXiv, 1509.7206 | | Other source: | [GID 1650807] 1505.6953 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER