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

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.
978-3-319-45993-6
978-3-319-45994-3
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11567/893559
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact