Theoretical Aspects of Computing - ICTAC 2009

Static analysis may cause state space explosion problem. In this paper we demonstrate how ordinary differential equations can be used to check the deadlocks and boundedness of the programs. We hope that our method can avoid explosion of state space entirely. A concurrent program is represented by a family of differential equations of a restricted type, where each equation describes the program state change. This family of equations are shown analytically to have a unique solution. Each program state is measured by a time-dependent function that indicates the extent to which the state can be reached in execution. It is shown that 1) a program deadlocks iff every state measure converges to either 0 or 1 as time increases. Thus instead of exploring states, the solution of a family of differential equations is analyzed. 2) a program is bounded iff every state measure converges to a bounded nonnegative number.

Algorithms are different from programs and should not be described with programming languages. The only simple alternative to programming languages has been pseudo-code. PlusCal is an algorithm language that can be used right now to replace pseudo-code, for both sequential and concurrent algorithms. It is based on the TLA⁺ specification language, and a PlusCal algorithm is automatically translated to a TLA⁺ specification that can be checked with the TLC model checker and reasoned about formally.

“Classical” program development by refinement [12,2,3] is a technique for ensuring that source-level program code remains faithful to the semantic goals set out in its corresponding specification. Until recently the method has not extended to security-style properties, principally because classical refinement semantics is inadequate in security contexts [7].

The Shadow semantics introduced by Morgan [13] is an abstraction of probabilistic program semantics [11], and is rich enough to distinguish between refinements that do preserve noninterference security properties and those that don’t. In this paper we give a formal development of Private Information Retrieval [4]; in doing so we extend the general theory of secure refinement by introducing a new kind of security annotation for programs.

Formal verification is the holy grail of software validation. Practical applications of verification run into two major challenges. The first challenge is in writing detailed specifications, and the second challenge is in scaling verification algorithms to large software. In this talk, we present possible approaches to address these problems:

We define a type and effect system for a λ-calculus extended with side effects, in the form of primitives for creating and accessing resources. The analysis correctly over-approximates the sequences of resource accesses performed by a program at run-time. To accurately analyse the binding between the creation of a resource and its accesses, our system exploits a new class of types. Our ν-types have the form νN. τ ⊳ H, where the names in N are bound both in the type τ and in the effect H, that represents the sequences of resource accesses.

Online trading invariably involves dealings between strangers, so it is important for one party to be able to judge objectively the trustworthiness of the other. In such a setting, the decision to trust a user may sensibly be based on that user’s past behaviour. We introduce a specification language based on linear temporal logic for expressing a policy for categorising the behaviour patterns of a user depending on its transaction history. We also present an algorithm for checking whether the transaction history obeys the stated policy. To be useful in a real setting, such a language should allow one to express realistic policies which may involve parameter quantification and quantitative or statistical patterns. We introduce several extensions of linear temporal logic to cater for such needs: a restricted form of universal and existential quantification; arbitrary computable functions and relations in the term language; and a “counting” quantifier for counting how many times a formula holds in the past. We then show that model checking a transaction history against a policy, which we call the history-based transaction monitoring problem, is PSPACE-complete in the size of the policy formula and the length of the history, assuming that the underlying interpreted functions and relations are polynomially computable. The problem becomes decidable in polynomial time when the policies are fixed. We also consider the problem of transaction monitoring in the case where not all the parameters of actions are observable. We formulate two such “partial observability” monitoring problems, and show their decidability under certain restrictions.

Modal transition systems (MTS), a specification formalism introduced more than 20 years ago, has recently received a considerable attention in several different areas. Many of the fundamental questions related to MTSs have already been answered. However, the problem of the exact computational complexity of thorough refinement checking between two finite MTSs remained unsolved.

We settle down this question by showing EXPTIME-completeness of thorough refinement checking on finite MTSs. The upper-bound result relies on a novel algorithm running in single exponential time providing a direct goal-oriented way to decide thorough refinement. If the right-hand side MTS is moreover deterministic, or has a fixed size, the running time of the algorithm becomes polynomial. The lower-bound proof is achieved by reduction from the acceptance problem of alternating linear bounded automata and the problem remains EXPTIME-hard even if the left-hand side MTS is fixed.

Sequential programs under execution produce behaviours to be controlled by some execution environment. Threads as considered in basic thread algebra model such behaviours: upon each action performed by a thread, a reply from an execution environment – which takes the action as an instruction to be processed – determines how the thread proceeds. In this paper, we are concerned with the case where the execution environment is remote: we study some transmission protocols for passing instructions from a thread to a remote execution environment.

We design a deadlock-free semantics for a concurrent, functional and imperative programming language where locks are implicitly and univocally associated with pointers. The semantics avoids unsafe states by relying on a static analysis of programs, by means of a type and effect system. The system uses singleton reference types, which allow us to have a precise information about the pointers that are anticipated to be locked by an expression.

In higher-order process calculi the values exchanged in communications may contain processes. There are only two capabilities for received processes: execution and forwarding. Here we propose a limited form of forwarding: output actions can only communicate the parallel composition of statically known closed processes and processes received through previously executed input actions. We study the expressiveness of a higher-order process calculus featuring this style of communication. Our main result shows that in this calculus termination is decidable while convergence is undecidable.

The hairpin completion is a natural operation of formal languages which has been inspired by molecular phenomena in biology and by DNA-computing. The hairpin completion of a regular language is linear context-free and we consider the problem to decide whether the hairpin completion remains regular. This problem has been open since the first formal definition of the operation.

In this paper we present a positive solution to this problem. Our solution yields more than decidability because we present a polynomial time procedure. The degree of the polynomial is however unexpectedly high, since in our approach it is more than n ¹⁴. Nevertheless, the polynomial time result is surprising, because even if the hairpin completion \(\mathcal{H}\) of a regular language L is regular, there can be an exponential gap between the size of a minimal DFA for L and the size of a smallest NFA for \(\mathcal{H}\).

We define context-free grammars with Büchi acceptance condition generating languages of countable words. We establish several closure properties and decidability results for the class of Büchi context-free languages generated by these grammars. We also define context-free grammars with Müller acceptance condition and show that there is a language generated by a grammar with Müller acceptance condition which is not a Büchi context-free language.

Many software applications are based on collaborating, yet competing, agents or virtual organisations exchanging services. Contracts, expressing obligations, permissions and prohibitions of the different actors, can be used to protect the interests of the organisations engaged in such service exchange. However, the potentially dynamic composition of services with different contracts, and the combination of service contracts with local contracts can give rise to unexpected conflicts, exposing the need for automatic techniques for contract analysis. In this paper we look at automatic analysis techniques for contracts written in the contract language \(\mathcal{CL}\). We present a trace semantics of \(\mathcal{CL}\) suitable for conflict analysis, and a decision procedure for detecting conflicts (together with its proof of soundness, completeness and termination). We also discuss its implementation and look into the applications of the contract analysis approach we present. These techniques are applied to a small case study of an airline check-in desk.

Modal Transition Systems (MTS) are an extension of Labelled Transition Systems (LTS) that distinguish between required, proscribed and unknown behaviour and come equipped with a notion of refinement that supports incremental modelling where unknown behaviour is iteratively elaborated into required or proscribed behaviour. The original formulation of MTS introduces two alternative semantics for MTS, strong and weak, which require MTS models to have the same communicating alphabet, the latter allowing the use of a distinguished unobservable action. In this paper we show that the requirement of fixing the alphabet for MTS semantics and the treatment of observable actions are limiting if MTS are to support incremental elaboration of partial behaviour models. We present a novel semantics, branching alphabet semantics, for MTS inspired by branching LTS equivalence, we show that some unintuitive refinements allowed by weak semantics are avoided, and prove a number of theorems that relate branching refinement with alphabet refinement and consistency. These theorems, which do not hold for other semantics, support the argument for considering branching implementation of MTS as the basis for a sound semantics to support behaviour model elaboration.

Regular expressions with numerical constraints are an extension of regular expressions, allowing to bound numerically the number of times that a subexpression should be matched. Expressions in this extension describe the same languages as the usual regular expressions, but are exponentially more succinct.

We define a class of finite automata with counters and a deterministic subclass of these. Deterministic finite automata with counters can recognize words in linear time. Furthermore, we describe a subclass of the regular expressions with numerical constraints, a polynomial-time test for this subclass, and a polynomial-time construction of deterministic finite automata with counters from expressions in the subclass.

In the recent years, several new classes of contextual grammars have been introduced to give an appropriate model description to natural languages. With this aim, some new families of contextual languages have been introduced based on maximal and depth-first conditions and analyzed in the framework of so-called mildly context sensitive languages. However, the relationship among these families of languages have not yet been analyzed in detail. In this paper, we investigate the relationship between the families of languages whose grammars are based on maximal and depth-first conditions. We prove an interesting result that all these families of languages are incomparable to each other, but they are not disjoint.

Testing from first-order specifications has mainly been studied for flat specifications, that are specifications of a single software module. However, the specifications of large software systems are generally built out of small specifications of individual modules, by enriching their union. The aim of integration testing is to test the composition of modules assuming that they have previously been verified, i.e. assuming their correctness. One of the main method for the selection of test cases from first-order specifications, called axiom unfolding, is based on a proof search for the different instances of the property to be tested, thus allowing the coverage of this property. The idea here is to use deduction modulo as a proof system for structured first-order specifications in the context of integration testing, so as to take advantage of the knowledge of the correctness of the individual modules.

An assume-guarantee verification method has been recognized as a promising approach to verify component-based software with model checking. The method is not only fitted to component-based software but also has a potential to solve the state space explosion problem in model checking. This method allows us to decompose a verification target into components so that we can model check each of them separately. In this method, assumptions which are environments of the components are generated. The number of states of the assumptions should be minimized because the computational cost of model checking is influenced by that number. Thus, we propose a method for generating minimal assumptions for the assume-guarantee verification of component-based software. The key idea of this method is finding the minimal assumptions in the search spaces of the candidate assumptions. These assumptions are seen as the environments needed for the components to satisfy a property and for the rest of the system to be satisfied. The minimal assumptions generated by the proposed method can be used to recheck the whole system at much lower computational cost. We have implemented a tool for generating the minimal assumptions. Experimental results are also presented and discussed.

In order to test a Finite State Machine (FSM), first we typically have to identify some short interaction sequences allowing to reach those states or transitions considered as critical. If these sequences are applied to an implementation under test (IUT), then equivalent states or transitions would be reached and observed in the implementation – provided that the implementation were actually defined as the specification. In this paper we study how to obtain such sequences in a scenario where previous configurations can be restored at any time. In general, this feature enables sequences to reach the required parts of the machine in less time, because some repetitions can be avoided. However, finding optimal sequences is NP-hard when configurations can be restored. We use an evolutionary method, River Formation Dynamics, to heuristically solve this problem.

We consider the problem of analyzing multi-threaded programs with recursive calls, dynamic creation of parallel procedures, and communication. We model such programs by Process Rewrite Systems (PRS) which are sets of term rewriting rules. Terms in this framework represent program control structures. The semantics of PRS systems is defined modulo structural equivalences on terms expressing properties of the operators appearing in the terms (idle process, sequential composition, and asynchronous parallel composition).

We consider the problem of reachability analysis of PRSs under constraints on the execution actions. This problem is undecidable even for regular constraints. [LS98] showed that it becomes decidable for decomposable constraints for the PRS subclass PA if structural equivalences are not taken into account. In this work, we go further and show that for decomposable constraints, we can compute tree automata representations of the constrained reachability sets for the whole class of PRS modulo different structural equivalences. Our results can be used to solve program (data flow) analysis and verification problems that can be reduced to the constrained reachability analysis problem.

Model programs are used as high-level behavioral specifications typically representing abstract state machines. For modeling reactive systems, one uses input-output model programs, where the action vocabulary is divided between two conceptual players: the input player and the output player. The players share the action vocabulary and make moves that are labeled by actions according to their respective model programs. Conformance between the two model programs means that the output (input) player only makes output (input) moves that are allowed by the input (output) players model program. In a bounded game, the total number of moves is fixed. Here model programs use a background theory \(\mathcal{T}\) containing linear arithmetic, sets, and tuples. We formulate the bounded game conformance checking problem, or BGC, as a theorem proving problem modulo \(\mathcal{T}\) and analyze its complexity.

The GSPeeDI tool implements a decision procedure for the reachability analysis of GSPDIs, planar hybrid systems whose dynamics is given by differential inclusions, and that are not restricted by the goodness assumption from previous work on the so-called SPDIs.

Unlike SPeeDI (a tool for reachability analysis of SPDIs) the underlying analysis of GSPeeDI is based on a breadth-first search algorithm, and it can handle more general systems.

We have designed and implemented LMNtal (pronounced “elemental”), a language based on hierarchical graph rewriting that allows us to encode diverse computational models involving concurrency, mobility and multiset rewriting. Towards its novel applications, the system has recently evolved into a model checker that employs LMNtal as the modeling language and PLTL as the specification language. The strengths of our LMNtal model checker are its powerful data structure, highly nondeterministic computation it can express, and virtually no discrepancy between programming and modeling languages. Models expressed in Promela, MSR, and Coloured Petri Nets can be easily encoded into LMNtal. The visualizer of the LMNtal IDE turned out to be extremely useful in understanding models by state space browsing. The LMNtal IDE has been used to run and visualize diverse examples taken from the fields of model checking, concurrency and AI search.