Overview

PAWS is a tool to analyse the behaviour of weighted automata and conditional transition systems. At its core PAWS is based on a generic implementation of algorithms for checking language equivalence in weighted automata and bisimulation in conditional transition systems. The tool is designed in such a way that arbitrary user-defined semirings can be employed. New semirings can be generated during run-time and the user can rely on numerous automatisation techniques to help with creating new semiring structures to use with PAWS’ algorithms. Basic semirings such as distributive complete lattices and fields of fractions can be defined by specifying few parameters, more exotic semirings can be built from other semirings or defined from scratch using a built-in semiring generator tool. In the most general case, users can define new semirings by programming (in C#) the base operations of the semiring and a procedure to solve linear equations and use their newly generated semiring in the analysis methods offered by PAWS.

The development of this tool is part of the BEMEGA project (related publications). The paper "PAWS: A Tool for the Analysis of Weighted Systems" is included in the publications of the QAPL 2017 workshop.

 

System requirements

Getting started with PAWS

In order to run PAWS, download it via the provided linke and unzip the files. After that you need to run the Analysis_Part.exe file in PAWS/Analysis_Part/bin/. For semiring generation you can switch to the generator component using the "Save and Generator" button.

Compiling PAWS

PAWS is implemented in C# and can be compiled for 32-bit version without any restrictions. 64-bit Compiling works only without the GraphViz library. It should be noted that manually implemented semirings, in the config files also have to be added, if one wants to use these within the semiring generator.

External Libaries and Projects

GraphViz and PAT.BDD

Usage

Currently, only a minimal tutorial is included, which is available pressing the "Help" button in the semiring generator.

Input and output

For loading and storing weighted automatas or generated semirings PAWS is using the MSDN serialization of C#. At the moment serialization for lattices on BDD is not supported. For source code generation we use CodeDOM.