We introduce a logic-based formalism to specify updates on arbitrary graphs. For the resulting language called GLog, we introduce an assertional language for reasoning about infinite sets of graph configurations in which we use reachability predicates to specify paths of arbitrary length. For the considered assertional language and a restricted class of update rules, we define a symbolic procedure to compute predecessor configurations.
Reachability predicates for graph assertions
Delzanno, Giorgio
2016-01-01
Abstract
We introduce a logic-based formalism to specify updates on arbitrary graphs. For the resulting language called GLog, we introduce an assertional language for reasoning about infinite sets of graph configurations in which we use reachability predicates to specify paths of arbitrary length. For the considered assertional language and a restricted class of update rules, we define a symbolic procedure to compute predecessor configurations.
File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
