一句话：提出实时能量函数的 *-连续 Kleene ω-代数，并据此静态判定实时能量自动机的可达性与 Büchi 接受性。
本文研究可随时间消耗与补充能量（或其他资源）的实时系统，其行为可由实时能量自动机描述。作者构建了一类实时能量函数的 *-连续 Kleene ω-代数，并与相应的自动机模型相结合，使能量与时间约束可用代数运算统一表达。借助近期关于 *-连续 Kleene ω-代数以及实时能量函数相关操作可计算性的结果，论文证明实时能量自动机的可达性和 Büchi 接受性可以在不进行动态搜索的情况下静态判定：判定过程仅需对实时能量函数进行代数操作。该工作为带时间与资源约束的 ω-正则性质验证提供了统一的代数框架与可判定性基础。
We develop a $^*$-continuous Kleene $\omega$-algebra of real-time energy functions. Together with corresponding automata, these can be used to model systems which can consume and regain energy (or other types of resources) depending on available time. Using recent results on $^*$-continuous Kleene $\omega$-algebras and computability of certain manipulations on real-time energy functions, it follows that reachability and B\"uchi acceptance in real-time energy automata can be decided in a static way which only involves manipulations of real-time energy functions.
@article{paperbot788,
title = {An $\omega$-Algebra for Real-Time Energy Problems},
author = {David Cachera and Uli Fahrenberg and Axel Legay},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 2},
year = {2019},
doi = {10.23638/lmcs-15(2:17)2019}
}