Counting Automata

Project Goal

Implement support for counting automata (CA) in Ultimate. Motivation: We would like to have efficient powerset alphabets and words with fixed repetitions.

Resources

Preprint that contains a formal definition of counting automata and explains the determinization operation.

2019APLAS - Holík,Lengál,Saarikivi,Turonová,Veanes,Vojnar - Succinct Determinisation of Counting Automata via Sphere Construction

Ultimate Installation

Ultimate Installation

Ultimate Web Interface

Automata library in web interface

Ultimate

Processing of Automata Script

1. AutomataScriptParser. Input: textual representation of .ats file, Output: Abstract syntax tree (AST)
2. AutomataScriptInterpreter. Input: AST, Construct automata in automata library data structures, use automata libarary to perform automata operations, Output: Status for each operation (success/failure), return value of print operation.

Project Phases

Project Planning

• Discuss the topic
• Read the paper (https://arxiv.org/abs/1910.01996v1) individually
• Work through the paper together for better understanding and to clarify misunderstandings

Concept

• Consider nondeterministic Finite Automaton (NFA) and operations such as intersection, union, concatenation, complement,...
• Write down examples of FSM for every operation
• Consider if and how the algorithms for these operations can be modified to suit CAs
• Write down the modified/new algorithms for CAs in detail
• Write down examples of CA for every operation

Implementation Preparation

• Install and configurate Ultimate
• Discuss data structures used in Ultimate for NFA and their textual representation
• Write down basic idea for CA data structures
• Write down concept for textual representation (use SMT-LIB for formulae)
• Construct such a representation for the examples used for operations
• Write down CA data structures more detailed and check if operations are suitable
• Construct a new, actually correct algorithm for union
• Consider how an intuitiv version of an acceptance test works (which might be inefficient and/or infinite)
• Consider how an intuitiv version of a transformation from CA into NFA works (might be infinite)
• Understand how ultimate can be used to test

Implementation

• Write pseudocode for our CA data structure
• Consider "AbstractNestedwordAutomatonAST" and implement a similar version for CA
• Write pseudocode for intersect, union and complement
• Implement the CA data structure
• Implement intersect, union and complement
• Write down the syntax for the CA parser (context free grammar)
• Write pseudocode for both versions of concatenation and implement the one which suits our data structure better
• Write pseudocode for the acceptance test
• Refine implementation of the CA data structure
• Implement the CA parser
• Implement the CA writer
• Implement the CA interpreter
• Implement the acceptance test
• Test and debug

Current tasks

• None

Information for Implementation Tasks

Automata script parser extension

Extend trunk/source/AutomataScriptParser/src/de/uni_freiburg/informatik/ultimate/plugins/source/automatascriptparser/AutomataTestFileGrammar.cup This file defines the context-free grammar for which the parser is build and explains the parser how the AST is build.

AST data structures for automata script files

• Implement a class analogously to AbstractNestedwordAutomatonAST
• This is NOT the automata library data structure for counting automata.
• No high-level data structures allowed!. Only Strings, Lists, Sets, Maps, Pairs, Relations, ...

Counting automata data structure in automata library

Use the class Counting Automata in the package de.uni_freiburg.informatik.ultimate.automata.counting Possibly useful classes in Ultimate:

• Term for SMT-LIB formulas,
• AffineTerm for integer terms if we want to have a more direct access to constants and counters, (conversion to and from Term already implemented)
• PolynomialRelation for binary integer relations, (conversion to and from Term already implemented)
• AbstractRelation our implementation for MAP<K, SET> (abstract class, HashRelation is "default" implementation)

Write text representation of counting automata

Implement #CountingAutomataTodo in class AutomatonDefinitionPrinter

Implement counting automata operations

• As an example, I added the class Intersect in the counting automata package (see #CountingAutomataTodo)
• Use the intersection method of mStateFactory to construct new states