Published: 29th July 2014
DOI: 10.4204/EPTCS.159
ISSN: 2075-2180

EPTCS 159

Proceedings 3rd Workshop on
GRAPH Inspection and Traversal Engineering
Grenoble, France, 5th April 2014

Edited by: Dragan Bošnački, Stefan Edelkamp, Alberto Lluch Lafuente and Anton Wijs

Preface
Alberto Lluch Lafuente, Anton Wijs, Dragan Bošnački and Stefan Edelkamp
Invited Presentation: Walking Back and Forth in Labelled Transition Systems
Radu Mateescu
1
Generating and Solving Symbolic Parity Games
Gijs Kant and Jaco van de Pol
2
Strategic Port Graph Rewriting: An Interactive Modelling and Analysis Framework
Maribel Fernández, Hélène Kirchner and Bruno Pinaud
15
Entity-Linking via Graph-Distance Minimization
Roi Blanco, Paolo Boldi and Andrea Marino
30
Graph- versus Vector-Based Analysis of a Consensus Protocol
Giorgio Delzanno, Arend Rensink and Riccardo Traverso
44
Specifying and Executing Optimizations for Parallel Programs
William Mansky, Dennis Griffith and Elsa L. Gunter
58
Graph Transformation Planning via Abstraction
Steffen Ziegert
71
Backwards State-space Reduction for Planning in Dynamic Knowledge Bases
Valerio Senni and Michele Stawowy
84

Preface

These are the proceedings of the Third Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014), which took place on April 5, 2014 in Grenoble, France, as a satellite event of the 17th European Joint Conferences on Theory and Practice of Software (ETAPS 2014).

The aim of GRAPHITE is to foster the convergence on research interests from several communities dealing with graph analysis in all its forms in computer science, with a particular attention to software development and analysis. Graphs are used to represent data and processes in many application areas, and they are subjected to various computational algorithms in order to analyze them. Just restricting the attention to the analysis of software, graph analysis algorithms are used, for instance, to verify properties using model checking techniques that explore the system's state space graph or static analysis techniques based on control flow graphs. Further application domains include games, planning, and network analysis. Very often, graph problems and their algorithmic solutions have common characteristics, independent of their application domain. The goal of this event is to gather scientists from different communities, who do research on graph analysis algorithms, such that awareness of each others' work is increased.

The first two workshops were held as satellite events of ETAPS 2012 and 2013. In 2009, the same motivation led to organising Dagstuhl Seminar 09491, entitled "Graph Search Engineering". The GRAPHITE workshop resulted from the overall success of that seminar.

This year, Radu Mateescu from the CONVECS team at INRIA Grenoble - Rhône-Alpes was our invited speaker. His talk was titled Walking Back and Forth in Labelled Transition Systems.

Besides that, we also had a call for technical papers. Each contribution went through a thorough reviewing process. For this, we would like to thank the GRAPHITE 2014 program committee members:

We also thank the external referees Harrie Jan Sander Bruggink, Sebastian Küpper, and Michele Stawowy for their help.

We thank all the authors of submitted papers for their contributions, and all accepted papers for the quick turnaround in producing the camera-ready copies included in this proceedings. Finally, we thank the editorial board of EPTCS, and the workshops chair of ETAPS 2014, Axel Legay, for their support.

Dragan Bošnački
Stefan Edelkamp
Alberto Lluch Lafuente
Anton Wijs


Walking Back and Forth in Labelled Transition Systems

Radu Mateescu (Inria Grenoble - Rhône-Alpes)

Graph exploration underlies several analysis problems defined on Labeled Transition Systems (LTSs), such as model checking, equivalence checking, tau-confluence reduction, pruning of undesirable behavior, etc. This talk gives an overview of the graph exploration techniques available in the CADP verification toolbox, their instantiation in verification tools (in particular, the Evaluator 4.0 and XTL model checkers), and their applications to the analysis of LTSs.