Parameterized Verification under Release Acquire is PSPACE-complete

We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. In the non-parameterized setting, access to atomic compare-and-swap (CAS) instructions renders the safety verification problem undecidable. In the light of this result, we consider parameterized systems consisting of an unbounded...

Formal modelling and verification of a multi-agent negotiation approach for airline operations control

This paper proposes and evaluates a new airline disruption management strategy using multi-agent system modelling, simulation, and verification. This new strategy is based on a multi-agent negotiation protocol and is compared with three airline strategies based on established industry practices. The application concerns Airline Operations...

Feasibility of a Knowledge-Based Engineering framework for the AEC industries

This paper presents the development of a novel computational framework with which expert analysis knowledge can be captured, stored and dynamically retrieved when required to determine the performance of a building design with respect to user-defined requirements. By subdividing the engineer's and designer's knowledge into discrete steps, and...

Finite Abstractions of Network Calculus Elements for Formal Verification of Network Bounds

This thesis presents a method to semi-automate the reasoning about network bounds, namely the backlog and delay. Network Calculus offers a rich theory for modeling network elements. Using the modeling techniques of network calculus, network elements are represented by discrete-time systems whose dynamics are linear in min-plus algebra. From the...

ifcModelCheck

On behalf of the BBR (German Federal Office for Building and Regional Planning) the development of an Industry Foundation Classes (IFC) based inspection tool was accomplished as application on an underlying work-in-progress development framework. By providing a machine-based checking process the tool ModelCheck was rolled out to meet demands...

Model checking GOAL agents

This thesis presents a novel approach to model checking of agent programs written in an agent programming language. The language we consider is GOAL. The novelty of the approach is that we implement model checking algorithms from scratch on top of the standard language interpreter. In contrast, in the literature on agent program verification,...