
<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>handle: 11588/572589
In formal verification and design, reasoning about substructures is a crucial aspect for several fundamental problems, whose solution often requires to select a portion of the model of interest on which to verify a specific property. In this paper, we present a new branching-time temporal logic, called Substructure Temporal Logic (STL*, for short), whose distinctive feature is to allow for quantifying over the possible substructure of a given structure. This logic is obtained by adding two new operators to CTL*, whose interpretation is given relative to the partial order induced by a suitable substructure relation. STL* turns out to be very expressive and allows to capture in a very natural way many well known problems, such as module checking, reactive synthesis and reasoning about games. A formal account of the model theoretic properties of the new logic and results about (un)decidability and complexity of related decision problems are also provided.
Formal verification, Temporal logics, Formal verification; Temporal logics
Formal verification, Temporal logics, Formal verification; Temporal logics
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 6 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
