the proceedings contain 15 papers. the special focus in this conference is on Mathematics of Program Construction. the topics include: Integrating programming, properties, and validation;polytypic values possess polyk...
ISBN:
(纸本)9783540677277
the proceedings contain 15 papers. the special focus in this conference is on Mathematics of Program Construction. the topics include: Integrating programming, properties, and validation;polytypic values possess polykinded types;the zip calculus;separation and reduction;reasoning about non-terminating loops using deadline commands;quantum programming;a coinductive approach to streams, automata, and power series;proving pointer programs in hoare logic;on guarded commands with fair choice;formal methods and dependability;liberating data refinement;theorems about composition;the universal resolving algorithm;metacomputation-based compiler architecture;a metalanguage for programming with bound names modulo renaming.
In this paper we show how model checking can be used for the verification of security protocols using a logic of belief. We model principals as processes able to have beliefs. the idea underlying the approach is to tr...
详细信息
ISBN:
(纸本)3540672826
In this paper we show how model checking can be used for the verification of security protocols using a logic of belief. We model principals as processes able to have beliefs. the idea underlying the approach is to treat separately the temporal evolution and the belief aspects of principals. therefore, when we consider the temporal evolution, belief formulae are treated as atomic propositions;while the fact that principal A has beliefs about another principal B is modeled as the fact that A has access to a representation of B as a process. As a motivating example, we use the framework proposed to formalize the Andrew protocol.
Inductive logicprogramming (11,P), as any other machine learning or KDD methods, has to deal with imperfect data when applied to real-world problems. Granular Computing (GrC) is a superset of various theories (such a...
详细信息
ISBN:
(纸本)0964345692
Inductive logicprogramming (11,P), as any other machine learning or KDD methods, has to deal with imperfect data when applied to real-world problems. Granular Computing (GrC) is a superset of various theories (such as rough sets, fuzzy sets and interval computation) used to handle incompleteness, uncertainty, vagueness, etc. in information systems. this paper investigates the feasibility of applying GrC (especially the rough set theory) to deal with imperfect data in ILP. We list various kinds of imperfect data in ILP (including noise data, too sparse data, missing data, indiscernible data, and too strict bias). For each kind of imperfect data, we try to point out the resulting problem and the potential solution using GrC (or a particular form of GrC such as the rough set theory). the presentation includes formalisms suggested by the authors or other researchers, as well as some general ideas which may give rise to more concrete results in future research.
Part of the recent work in AI planning is concerned withthe development of algorithms that regard planning as a combinatorial search problem. the underlying representation language is basically propositional logic. W...
详细信息
ISBN:
(纸本)3540678662
Part of the recent work in AI planning is concerned withthe development of algorithms that regard planning as a combinatorial search problem. the underlying representation language is basically propositional logic. While this is adequate for many domains, it is not clear if it remains so for problems that involve numerical constraints, or optimization of complex objective functions. Moreover, the propositional representation imposes restrictions on the domain knowledge that can be utilized by these approaches. In order to address these issues, we propose moving to the more expressive language of Integer programming (IP). We show how capacity constraints can be easily encoded into linear 0-1 inequalities and how rich forms of domain knowledge can be compactly represented and computationally exploited by IP solvers. then we introduce a novel heuristic search method based on the linear programming relaxation. Finally, we present the results of our experiments with a classical relaxation-based IP solver and a logic-based 0-1 optimizer.
this paper formalises a semantics for statements and expressions (in sequential imperative languages) which includes non-termination, normal termination and abrupt termination (e.g. because of an exception, break, ret...
详细信息
ISBN:
(纸本)3540672613
this paper formalises a semantics for statements and expressions (in sequential imperative languages) which includes non-termination, normal termination and abrupt termination (e.g. because of an exception, break, return or continue). this extends the traditional semantics underlying e.g. Hoare logic, which only distinguishes termination and non-termination. An extension of Hoare logic is elaborated that includes means for reasoning about abrupt termination (and side-effects). It prominently involves rules for reasoning about while loops, which may contain exceptions, breaks, continues and returns. this extension applies in particular to Java. As an example, a standard pattern search algorithm in Java (involving a while loop with returns) is proven correct using the proof-tool PVS.
In this paper, we present a generic tool, called FMona, for expressing validation methods. we illustrate its use through the expression of the abstraction technique and its application to infinite or parameterized spa...
详细信息
ISBN:
(纸本)3540672826
In this paper, we present a generic tool, called FMona, for expressing validation methods. we illustrate its use through the expression of the abstraction technique and its application to infinite or parameterized space problems. After a review of the basic results concerning transition systems, we show how abstraction can be expressed within FMona and used to build a reduced system with decidable properties. the FMona tool is used to express the validation steps leading to synthesis of a finite abstract system;then SMV and/or Mona validate its properties.
this paper describes an experience in formal specification and fault tolerant behavior validation of a railway critical system. the work, performed in the context of a real industrial project, had the following main t...
详细信息
ISBN:
(纸本)3540672826
this paper describes an experience in formal specification and fault tolerant behavior validation of a railway critical system. the work, performed in the context of a real industrial project, had the following main targets: (a) to validate specific safety properties in the presence of byzantine system components or of some hardware temporary faults;(b) to design a formal model of a critical railway system at a right level of abstraction so that could be possible to verify certain safety properties and at the same time to use the model to simulate the system. For the model specification we used the PROMELA language, while the verification was performed using the SPIN model checker. Safety properties were specified by means of both assertions and temporal logic formulae. To make the problem of validation tractable in the SPIN environment, we used ad hoc abstraction techniques.
this research shows how Constraint logicprogramming can form the basis of a knowledge elicitation tool for the development of adaptive tests. A review of literature reveals that adaptive testing has, in recent years,...
ISBN:
(纸本)3540676554
this research shows how Constraint logicprogramming can form the basis of a knowledge elicitation tool for the development of adaptive tests. A review of literature reveals that adaptive testing has, in recent years, been used as a student modelling tool in intelligent tutoring systems. Efforts in the construction and delivery of such tests have involved the use of state-space type constructs, such as granularity hierarchies and knowledge spaces, to represent a syllabus. the use of Bayesian probability networks has been proposed as a technique for finding an optimal route through these ”spaces” so as to find the shortest sequence of problems to put to the student being evaluated. the research presented here sets out to use ”expert emulation” as means of performing the same tasks. the aim is to construct an adaptive test in order to model a student’s knowledge, skills and tutorial requirements. the context is the development of such a system to support autonomous revision for examination in a particular domain in elementary mathematics.
Our approach of rule-based refinement(1) provides a formal description for the stepwise system development based on Petri nets. Rules with a left-hand and a right-hand side allow replacing subnets in a given algebraic...
详细信息
ISBN:
(纸本)3540672613
Our approach of rule-based refinement(1) provides a formal description for the stepwise system development based on Petri nets. Rules with a left-hand and a right-hand side allow replacing subnets in a given algebraic high-level net system. the extension of these rules supports the preservation of system properties. In this paper we extend the preservation of safety properties significantly. We define rules, that introduce new safety properties. In our new approach we propose first the verification of properties at the moment they can be expressed and then their preservation further on. Hence, properties can be checked as long as the system is still small. Moreover, introducing properties allows checking these for the relevant subpart only. Changes that are required later on can be treated the same way and hence preserve the system properties. Hence, we have made a step towards a formal technique for the stepwise system development during analysis and design.
the proceedings contain 30 papers. the special focus in this conference is on logicprogramming and Nonmonotonic Reasoning. the topics include: Fixed parameter complexity in AI and nonmonotonic reasoning;classifying s...
ISBN:
(纸本)3540667490
the proceedings contain 30 papers. the special focus in this conference is on logicprogramming and Nonmonotonic Reasoning. the topics include: Fixed parameter complexity in AI and nonmonotonic reasoning;classifying semi-normal default logic on the basis of its expressive power;locally determined logic programs;annotated revision programs;belief, knowledge, revisions, and a semantics of non-monotonic reasoning;an argumentation framework for reasoning about actions and changes;representing transition systems by logic programs;transformations of logic programs related to causality and planning;from causal theories to logic programs;monotone expansion of updates in logical databases;updating extended logic programs through abduction;pushing goal derivation in DLP computations;linear tabulated resolution for well founded semantics;minimal founded semantics for disjunctive logicprogramming;on the role of negation in choice logic programs;approximating reiter’s default logic;coherent well-founded annotated logic programs;many-valued disjunctive logic programs with probabilistic semantics;extending disjunctive logicprogramming by T-norms;extending the stable model semantics with more expressive rules;stable model semantics for weight constraint rules;towards first-order nonmonotonic reasoning;comparison of sceptical NAF-free logicprogramming approaches;characterizations of classes of programs by three-valued operators;using LPNMR for problem specification and code generation;answer set planning;world-modeling vs. world-axiomatizing and extended inheritance techniques to solve real-world problems.
暂无评论