Author name cluster

Bruno Lopes

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

FLAP Journal 2022 Journal Article

A logical framework to reason about Reo circuits.

Erick Simas Grilo
Daniel Toledo
Bruno Lopes

Reo is a graphic-based coordination modelling language which aims to capture and model the interaction between pieces of software, using structures known as channels. The fact that Reo has been used to model many real-world situations, from software components to Smart Cities entities, has attracted attention from researchers, resulting in a great effort directed in its formalization in order to verify and certify properties of Reo circuits. This work presents a constructive formalization in Coq of Reo’s formal semantics (based on Constraint Automata) and a formalization in the nuXmv model checker, both with a composition operation and with tools to automate the process. We describe the formalizations and present some usage examples with experimental results.

Details

TCS Journal 2018 Journal Article

Towards reasoning about Petri nets: A Propositional Dynamic Logic based approach

Mario Benevides
Bruno Lopes
Edward Hermann Haeusler

This work extends our previous work [4, 22] with the iteration operator. This new operator allows for representing more general networks and thus enhancing the former propositional logic for Petri nets. We provide an axiomatization and a new semantics, prove soundness and completeness with respect to its semantics and the EXPTIME-Hardness of its satisfiability problem, present a linear model checking algorithm and show that its satisfiability problem is in 2EXPTIME. In order to illustrate its usage, we also provide some examples.

Details DOI