@inbook{c639f194c48142db92b8fa221cce60eb,
title = "Refining the Safety-Liveness Classification of Temporal Properties According to Realizability",
abstract = "In the specification approach focus (see [2]), systems are specified by interface predicates which relate input histories to output histories. In such interface predicates, required safety and liveness properties of systems are formulated for the output histories in terms of their dependencies on the properties of input histories. In the following, we show how safety and liveness properties in systems specifications relate to questions of refinement, causality, and realizability. In particular, we study the effect of logical operations onto safety and liveness properties and how this relates to specification refinement. In addition, we analyze which safety and liveness properties used in implicative formulas can be realized by Moore machines. The requirements about the realizability by Moore machines are reflected in respective refinements simplifying or strengthening the original specifications.",
keywords = "Causality, Liveness, Realizability, Refinement, Safety",
author = "Manfred Broy",
note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.",
year = "2021",
doi = "10.1007/978-3-030-87348-6\_2",
language = "English",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "10--31",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}