This research line consists regards model checking approaches where:

  • systems are described by means of graph, graph transformation systems (aka graph rewrite systems, aka graph grammars)
  • system properties are specified by means of logics that involve structural (or spatial) and temporal modal operators
  • verification algorithms deal with graphical nature of models and their specificaiton

More details on this topic can be found in the following documents and the references therein:

  • Exploiting over- and under-approximations for infinite-state counterpart models
     Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin
    International Conference on Graph Transformation (ICGT’12)
  • State Space c-Reductions of Concurrent Systems in Rewriting Logic
     Alberto Lluch Lafuente, José Meseguer, Andrea Vandin
    International Conference on Formal Engineering Methods (ICFEM’12)
  • Modelling and analyzing adaptive self-assembling strategies with Maude
     Roberto Bruni, Andrea Corradini, Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin
    International Workshop on Rewriting Logic and its Applications (WRLA’12)
  • Counterpart semantics for a second-order mu-calculus
     Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin
    Fundamenta Informaticae
  • Towards a Maude Tool for Model Checking Temporal Graph Properties
     Alberto Lluch Lafuente, Andrea Vandin
    International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT’10)
  • A Lewisian Approach to the Verification of Adaptive Systems
     Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin
    ‘Another World is Possible’, Conference on David Lewis, Rivista Italiana di Filosofia Analitica Junior 2:2 (2011)
     
  • Counterpart semantics for a second-order mu-calculus
    Fabio Gadducci, Alberto Lluch Lafuente, Andrea Vandin
    International Conference on Graph Transformation (ICGT’10)
  • Graphical Encoding of a Spatial Logic for the pi-calculus
    Fabio Gadducci, Alberto Lluch Lafuente, Proceeedings of the 2nd Conference on Algebra and Coalgebra in Computer Science (CALCO’07), 2007.
    abstract     bib
  • A Temporal Graph Logic for the Verification of Graph Transformation Systems
    Paolo Baldan, Andrea Corradini, Barbara König, Alberto Lluch Lafuente, WADT’06, 2007.
    abstract     bib
  • Heuristic Search for the Analysis of Graph Transition Systems
    Stefan Edelkamp, Shahid Jabbar, Alberto Lluch Lafuente, International Conference on Graph Transformation (ICGT) Natal, 2006.
    abstract bib
  • A Logic for Application Level QoS
    Dan Hirsch, Alberto Lluch-Lafuente, Emilio Tuosto, Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages, Elsevier Electronic Notes on Theoretical Computer Science, 2006. bib
  • Graphical Verification of a Spatial Logic for the pi-calculus
    Fabio Gadducci, Alberto Lluch, 1st Workshop on Graph Transformation for Verification and Concurrency (GT-VC 2005), August 2005.
    abstract     bib
  • A logic for graphs with QoS
    Gianluigi Ferrari, Alberto Lluch Lafuente, 1st Workshop on Views On Designing Complex Architectures, September 2004.
    abstract bib