Probability features increasingly often in software and hardware systems: it is used in distributed co-ordination and routing problems, to model fault-tolerance and performance, and to provide adaptive resource manage...
详细信息
ISBN:
(纸本)0769518842
Probability features increasingly often in software and hardware systems: it is used in distributed co-ordination and routing problems, to model fault-tolerance and performance, and to provide adaptive resource management strategies. Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying probabilistic specifications such as "leader election is eventually resolved with probability 1", "the chance of shutdown occurring is at most 0.01% ", and "the probability that a message will be delivered within 30ms is at least 0.75". A probabilistic model checker calculates the probability of a given temporal logic property being satisfied, as opposed to validily. In contrast to conventional model checkers, which rely on reachabiliiy analysis of the underlying transition system graph, probabilistic model checking additionally involves numerical solutions of linear equations and linear programming problems. This paper reports our experience with implementing PRISM (***/(similar to)dxp/ prism/), a Probabilistic Symbolic Model Checker demonstrates its usefulness in analysing real-world probabilistic protocols, and outlines future challenges for this research direction.
Pruning provides an important tool for control of non-determinism in Prolog systems. Current Tabled Prolog systems improve Prolog’s evaluation strategy in several ways, but lack satisfactory support for pruning opera...
详细信息
Significant advances have recently been made in the area of updates of logic programs, and, more generally, updates of knowledge bases and their applications. Accordingly, the journal theory and practice of logic Prog...
Significant advances have recently been made in the area of updates of logic programs, and, more generally, updates of knowledge bases and their applications. Accordingly, the journal theory and practice of logic programming has planned a special issue on Change in Knowledge Bases, tentatively scheduled to appear at the beginning of ***-quality papers are sought containing either original research results or offering an insightful synthesis of past work on various aspects of change in knowledge *** and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. Surveys and comparison of state of the art techniques are also solicited.
The proceedings contain 126 papers. The special focus in this conference is on Principles and practice of Constraint programming. The topics include: Recent progress in propositional reasoning and search;a new applica...
ISBN:
(纸本)3540202021
The proceedings contain 126 papers. The special focus in this conference is on Principles and practice of Constraint programming. The topics include: Recent progress in propositional reasoning and search;a new application area for search algorithms;languages versus packages for constraint problem solving;constraint patterns;control abstractions for local search;improved algorithms for counting solutions in constraint satisfaction problems;boosting chaff’s performance by incorporating CSP heuristics;efficient CNF encoding of boolean cardinality constraints;a two-stage hybrid algorithm for pickup and delivery vehicle routing problems with time windows;solving finite domain constraint hierarchies by local consistency and tree search;a constraint programming application to staff scheduling in health care;constraint-based optimization with the minimax decision criterion;an algebraic approach to multi-sorted constraints;polynomial-time algorithms;box constraint collections for adhoc constraints;propagation redundancy in redundant modelling;complexity and multimorphisms;constraint satisfaction differential problems;a wealth of sat distributions with planted assignments;redundant modeling for the quasigroup completion problem;open constraint optimization;constraints for breaking more row and column symmetries;generic SBDD using computational group theory;using stochastic local search to solve quantified boolean formulae;solving max-SAT as weighted CSP;constraint reasoning over strings;tractability by approximating constraint languages;constraints for probabilistic reasoning in logicprogramming;constraint programming for modelling and solving modal satisfiability;distributed forward checking and a new class of binary CSPs for which arc-consistency is a decision procedure.
A goal-independent suspension analysis is presented that infers a class of goals for which a logic program with delays can be executed without suspension. The crucial point is that the analysis does not verify that an...
详细信息
Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. It is thus natural to develop a Hoare calculus for reasoning about computational mon...
详细信息
This paper addresses the problem of establishing temporal properties of programs written in languages, such as Java, that make extensive use of the heap to allocate—and deallocate—new objects and threads. Establishi...
详细信息
KLAIM (Kernel Language for Agents Interaction and Mobility) is an experimental language specifically designed to program distributed systems consisting of several mobile components that interact through multiple distr...
详细信息
ISBN:
(纸本)3540205837
KLAIM (Kernel Language for Agents Interaction and Mobility) is an experimental language specifically designed to program distributed systems consisting of several mobile components that interact through multiple distributed tuple spaces. KLAIM primitives allow programmers to distribute and retrieve data and processes to and from the nodes of a net. Moreover, localities are first-class citizens that can be dynamically created and communicated over the network. Components, both stationary and mobile, can explicitly refer and control the spatial structures of the network. This paper reports the experiences in the design and development of KLAIM. Its main purpose is to outline the theoretical foundations of the main features of KLAim and its programming model. We also present a modal logic that permits reasoning about behavioural properties of systems and various type systems that help in controlling agents movements and actions. Extensions of the language in the direction of object oriented programming are also discussed together with the description of the implementation efforts which have lead to the current prototypes.
The proceedings contain 27 papers. The special focus in this conference is on Software components, Mobile computing, Aspect and object-oriented programming, Distributed and web applications, Software measurements, For...
ISBN:
(纸本)3540008993
The proceedings contain 27 papers. The special focus in this conference is on Software components, Mobile computing, Aspect and object-oriented programming, Distributed and web applications, Software measurements, Formal verification, Analysis and testing and Model integrations and extensions. The topics include: An ontology for software component matching;a description language for composable components;a logical basis for the specification of reconfigurable component-based systems;an overall system design approach doing object-oriented modeling to code-generation for embedded electronic systems;composing specifications of event based applications;a Spatio-Temporal logic for the specification and refinement of mobile systems;spatial security policies for mobile agents in a sentient computing environment;towards UML-based formal specifications of component-based real-time software;modelling recursive calls with UML state diagrams;model-based development of web applications using graphical reaction rules;modular analysis of dataflow process networks;foundations of a weak measurement-theoretic approach to software measurement;an information-based view of representational coupling in object-oriented systems;a temporal approach to specification and verification of pointer data-structures;a program logic for handling java card’s transaction mechanism;automatic model driven animation of SCR specifications;probe mechanism for object-oriented software testing;integration of formal datatypes within state diagrams;towards a natural interoperability between XML and ER diagrams;detecting implied scenarios analyzing non-local branching choices and capturing overlapping, triggered, and preemptive collaborations using MSCs.
A method for finding bugs in object-oriented code is presented. It is capable of checking complex user-defined structural properties - that is, of the configuration of objects on the heap - and generates counterexampl...
详细信息
暂无评论