Related papers: On Termination of Polynomial Programs with Equalit…
We exhibit an algorithm to compute the strongest polynomial (or algebraic) invariants that hold at each location of a given affine program (i.e., a program having only non-deterministic (as opposed to conditional) branching and all of whose…
This paper investigates two related optimal input selection problems for fixed (non-switched) and switched structured systems. More precisely, we consider selecting the minimum cost of inputs from a prior set of inputs, and selecting the…
Immanants are polynomial functions of n by n matrices attached to irreducible characters of the symmetric group S_n, or equivalently to Young diagrams of size n. Immanants include determinants and permanents as extreme cases. Valiant proved…
Quantitative loop invariants are an essential element in the verification of probabilistic programs. Recently, multivariate Lagrange interpolation has been applied to synthesizing polynomial invariants. In this paper, we propose an…
We present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/non-termination proof approaches. We introduce an idea of termination prediction, which predicts…
The classic algorithm [Papadimitriou, J.ACM '81] for IPs has a running time $n^{O(m)}(m\cdot\max\{\Delta,\|\textbf{b}\|_{\infty}\})^{O(m^2)}$, where $m$ is the number of constraints, $n$ is the number of variables, and $\Delta$ and…
It is well known that many problems in interval computation are intractable, which restricts our attempts to solve large problems in reasonable time. This does not mean, however, that all problems are computationally hard. Identifying…
We study the following problem: given a class of logic programs C, determine the maximum number of stable models of a program from C. We establish the maximum for the class of all logic programs with at most n clauses, and for the class of…
Given an implicational base, a well-known representation for a closure system, an inconsistency binary relation over a finite set, we are interested in the problem of enumerating all maximal consistent closed sets (denoted by MCCEnum for…
We consider nonlinear model predictive control (MPC) with multiple competing cost functions. In each step of the scheme, a multiobjective optimal control problem with a nonlinear system and terminal conditions is solved. We propose an…
Polynomial optimization encompasses a broad class of problems in which both the objective function and constraints are polynomial functions of the decision variables. In recent years, a substantial body of research has focused on…
Deciding termination is a fundamental problem in the analysis of probabilistic imperative programs. We consider the qualitative and quantitative probabilistic termination problems for an imperative programming model with discrete…
Partially Observable Markov Decision Processes (POMDPs) are powerful models for sequential decision making under transition and observation uncertainties. This paper studies the challenging yet important problem in POMDPs known as the…
We introduce the class of constant probability (CP) programs and show that classical results from probability theory directly yield a simple decision procedure for (positive) almost sure termination of programs in this class. Moreover,…
Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it…
We consider the problem of expected cost analysis over nondeterministic probabilistic programs, which aims at automated methods for analyzing the resource-usage of such programs. Previous approaches for this problem could only handle…
We introduce a system of monadic affine sized types, which substantially generalise usual sized types, and allows this way to capture probabilistic higher-order programs which terminate almost surely. Going beyond plain, strong…
Following a polynomial approach, many robust fixed-order controller design problems can be formulated as optimization problems whose set of feasible solutions is modelled by parametrized polynomial matrix inequalities (PMI). These…
Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for…
We consider the stochastic shortest path (SSP) problem for succinct Markov decision processes (MDPs), where the MDP consists of a set of variables, and a set of nondeterministic rules that update the variables. First, we show that several…