This paper is about an,application of hybrid logic to the following problem with reasoning about knowledge: how to axiomatize spaces of knowledge states over dense flows of time? We provide an answer to this question ...
详细信息
ISBN:
(纸本)3540002251
This paper is about an,application of hybrid logic to the following problem with reasoning about knowledge: how to axiomatize spaces of knowledge states over dense flows of time? We provide an answer to this question below, proving a corresponding completeness theorem. We will make essential use of the fact that the hybrid logical language is particularly suited to express, in the modal sense, first-order properties of frames.
In this paper we describe a constraint analyser for contextual rules. Contextual rules constitute a rule-based formalism that allows rewriting of terminals and/or non terminal sequences taking in account their context...
详细信息
ISBN:
(纸本)0769518672
In this paper we describe a constraint analyser for contextual rules. Contextual rules constitute a rule-based formalism that allows rewriting of terminals and/or non terminal sequences taking in account their context. The formalism allows also to refer to portions of text by means of exclusion zones, that is, patterns that are only specified by a maximun length and a set of not allowed categories. The constraint approach reveals particulary useful for this type of rules, as decisions can be taken under the hypothesis of non existence of the excluded categories. If these categories are finally deduced, all other categories inferred upon the non existence of the former ones are automatically eliminated. The parser has been implemented using Constraint Handling Rules. Some results with a set of rules oriented to the segmentation of texts in propositions are shown.
The proceedings contain 26 papers. The special focus in this conference is on Formal Techniques for Networked and Distributed Systems. The topics include: Bounded model checking for timed systems;submodule constructio...
ISBN:
(纸本)9783540361350
The proceedings contain 26 papers. The special focus in this conference is on Formal Techniques for Networked and Distributed Systems. The topics include: Bounded model checking for timed systems;submodule construction for specifications with input assumptions and output guarantees;mechanical translation of i/o automaton specifications into first-order logic;a nested depth first search algorithm for model checking with symmetry reduction;congruent weak conformance, a partial order among processes;formal test purposes and the validity of test cases;ntif: A general symbolic model for communicating sequential processes with data;from states to transitions: Improving translation of ltl formulae to büchi automata;a compositional sweep-line state space exploration method;a formal venture into reliable multicast territory;innovative verification techniques used in the implementation of a third-generation 1.1ghz 64b microprocessor;encoding pamr into (Timed) efsms;a distributed partial order reduction algorithm;system test synthesis from uml models of distributed software;use of logic to describe enhanced communications services;on combining the persistent sets method with the covering steps graph method;verification of event-based synchronization of specc description using difference decision diagrams;protocol techniques for testing radiotherapy accelerators;modelling sip services using cress;verifying reliable data transmission over umts radio interface with high level petri nets;c wolf – a toolset for extracting models from c programs;building tools for lotos symbolic semantics in maude;symmetric symbolic safety-analysis of concurrent software with pointer data structures.
We describe a formal tool based on a symbolic semantics for Full LOTOS, where specifications without restrictions in their data types can be executed. The reflective feature of rewriting logic and the metalanguage cap...
详细信息
ISBN:
(数字)9783540361350
ISBN:
(纸本)3540001417
We describe a formal tool based on a symbolic semantics for Full LOTOS, where specifications without restrictions in their data types can be executed. The reflective feature of rewriting logic and the metalanguage capabilities of Maude make it possible to implement the whole tool in the same semantic framework, and have allowed us to implement the LOTOS operational semantics, to integrate it with ACT ONE specifications, and to build an entire environment with. parsing, pretty printing, and input/output processing of LOTOS specifications. Our aim has been to implement a formal tool that can be used by everyone without knowledge of the concrete implementation, but where the semantics representation is at so high level that can be understood and modified by everyone that knows about operational semantics.
We describe a tool that improves the process of verifying relations between descriptions of a distributed algorithm at different levels of abstraction using interactive proof assistants. The tool automatically transla...
详细信息
New functionality is added to telecommunications systems in the form of features or services. However, this is a very provider-centric approach, not giving much control to the user. We consider a logic that allows the...
详细信息
This paper presents a survey of existing event systems structured as a taxonomy of distributed event-based programming systems. Our taxonomy identifies a set of fundamental properties of event-based programming system...
详细信息
This paper presents a survey of existing event systems structured as a taxonomy of distributed event-based programming systems. Our taxonomy identifies a set of fundamental properties of event-based programming systems and categorizes them according to the event model and event service criteria. The event service is further classified according to its organization and interaction model, as well as other functional and non-functional features.
We focus on an important problem in ubiquitous computing, namely, programming support for the distributed heterogeneous computing elements that make up this environment. We address the interactive, dynamic, and stream...
详细信息
We focus on an important problem in ubiquitous computing, namely, programming support for the distributed heterogeneous computing elements that make up this environment. We address the interactive, dynamic, and stream-oriented nature of this application class and develop appropriate computational abstractions in the D-Stampede distributed programming system. The key features of D-Stampede include indexing data streams temporally, correlating different data streams temporally, performing automatic distributed garbage collection of unnecessary stream data, supporting high performance by exploiting hardware parallelism where available, supporting platform and language heterogeneity, and dealing with application level dynamism. We discuss the features of D-Stampede, the programming ease it affords, and its performance.
We present a method of timestamping messages and events in synchronous computations that capture the order relationship with vectors of size less than or equal to the size of the vertex cover of the communication topo...
详细信息
We present a method of timestamping messages and events in synchronous computations that capture the order relationship with vectors of size less than or equal to the size of the vertex cover of the communication topology of the system. Our method is fundamentally different from the techniques of Fidge (1989) and Mattern (1989). The timestamps in our method do not use one component per process but still guarantee that the order relationship is captured accurately. Our algorithm is online and only requires piggybacking of timestamps on program messages. It is applicable to all programs that either use programming languages based on synchronous communication such as CSP or use synchronous remote procedure calls.
We propose the notion of invariant consistency that allows programmers to specify inter-process ordering requirements. In our approach, we allow a programmer to label a program and provide an ordering specification. I...
详细信息
We propose the notion of invariant consistency that allows programmers to specify inter-process ordering requirements. In our approach, we allow a programmer to label a program and provide an ordering specification. In particular, we associate a counter count/sub l/ with each label l that counts the number of times the operation labeled l has been executed. The ordering specification is given by an invariant on these counters.
暂无评论