Tag Archives: Programming Languages

Extending probabilistic logic programming with continuous r.v.s, and a nice and brief introduction to programming logic and probabilistic inference

Steffen Michels, Arjen Hommersom, Peter J.F. Lucas, Marina Velikova, A new probabilistic constraint logic programming language based on a generalised distribution semantics, Artificial Intelligence, Volume 228, November 2015, Pages 1-44, ISSN 0004-3702, DOI: 10.1016/j.artint.2015.06.008.

Probabilistic logics combine the expressive power of logic with the ability to reason with uncertainty. Several probabilistic logic languages have been proposed in the past, each of them with their own features. We focus on a class of probabilistic logic based on Sato’s distribution semantics, which extends logic programming with probability distributions on binary random variables and guarantees a unique probability distribution. For many applications binary random variables are, however, not sufficient and one requires random variables with arbitrary ranges, e.g. real numbers. We tackle this problem by developing a generalised distribution semantics for a new probabilistic constraint logic programming language. In order to perform exact inference, imprecise probabilities are taken as a starting point, i.e. we deal with sets of probability distributions rather than a single one. It is shown that given any continuous distribution, conditional probabilities of events can be approximated arbitrarily close to the true probability. Furthermore, for this setting an inference algorithm that is a generalisation of weighted model counting is developed, making use of SMT solvers. We show that inference has similar complexity properties as precise probabilistic inference, unlike most imprecise methods for which inference is more complex. We also experimentally confirm that our algorithm is able to exploit local structure, such as determinism, which further reduces the computational complexity.

Checking the behavior of robotic software (i.e., verification) and embedded sw in general, with a good related work on the issue

Lyons, D.M.; Arkin, R.C.; Shu Jiang; Tsung-Ming Liu; Nirmal, P., Performance Verification for Behavior-Based Robot Missions, Robotics, IEEE Transactions on , vol.31, no.3, pp.619,636, June 2015, DOI: 10.1109/TRO.2015.2418592.

Certain robot missions need to perform predictably in a physical environment that may have significant uncertainty. One approach is to leverage automatic software verification techniques to establish a performance guarantee. The addition of an environment model and uncertainty in both program and environment, however, means that the state space of a model-checking solution to the problem can be prohibitively large. An approach based on behavior-based controllers in a process-algebra framework that avoids state-space combinatorics is presented here. In this approach, verification of the robot program in the uncertain environment is reduced to a filtering problem for a Bayesian network. Validation results are presented for the verification of a multiple-waypoint and an autonomous exploration robot mission.

Interesting and gentle introduction to WCET analysis and synchronous design for hard real-time systems

Pascal Raymond, Claire Maiza, Catherine Parent-Vigouroux, Fabienne Carrier, Mihail Asavoae, 2015, Timing analysis enhancement for synchronous program, Real-Time Systems, Volume 51, Issue 2, pp 192-220, DOI: 10.1007/s11241-015-9219-y.

Real-time critical systems can be considered as correct if they compute both right and fast enough. Functionality aspects (computing right) can be addressed using high level design methods, such as the synchronous approach that provides languages, compilers and verification tools. Real-time aspects (computing fast enough) can be addressed with static timing analysis, that aims at discovering safe bounds on the worst-case execution time (WCET) of the binary code. In this paper, we aim at improving the estimated WCET in the case where the binary code comes from a high-level synchronous design. The key idea is that some high-level functional properties may imply that some execution paths of the binary code are actually infeasible, and thus, can be removed from the worst-case candidates. In order to automatize the method, we show (1) how to trace semantic information between the high-level design and the executable code, (2) how to use a model-checker to prove infeasibility of some execution paths, and (3) how to integrate such infeasibility information into an existing timing analysis framework. Based on a realistic example, we show that there is a large possible improvement for a reasonable computation time overhead.