This paper aims to provide a better formalism for describing properties of linked data structures (e.g., lists, trees, graphs), as well as the intermediate states that arise when such structures are destructively upda...
详细信息
ISBN:
(纸本)3540656995
This paper aims to provide a better formalism for describing properties of linked data structures (e.g., lists, trees, graphs), as well as the intermediate states that arise when such structures are destructively updated. The paper defines a new logic that is suitable for these purposes (called L-r, for "logic of reachability expressions"). We show that L-r is decidable, and explain how L-r relates to two previously defined structure-description formalisms ("path matrices" and "static shape graphs") by showing how an arbitrary shape descriptor from each of these formalisms can be translated into an L-r formula.
We show that Constraint logicprogramming (CLP) can serve as a conceptual basis and as a practical implementation platform for the model checking of infinite-state systems. Our contributions are: (1) a semantics-prese...
详细信息
ISBN:
(纸本)3540657037
We show that Constraint logicprogramming (CLP) can serve as a conceptual basis and as a practical implementation platform for the model checking of infinite-state systems. Our contributions are: (1) a semantics-preserving translation of concurrent systems into CLP programs, (2) a method for verifying safety and liveness properties on the CLP programs produced by the translation. We have implemented the method in a CLP system and verified well-known examples of infinite-state programs over integers, using here linear constraints as opposed to Presburger arithmetic as in previous solutions.
The situation calculus (SC) is a formalism for reasoning about action. Within SC, the notion of state of a given situation is usually characterized by the set of fluents that hold in that situation. However, this conc...
详细信息
ISBN:
(纸本)3540662464
The situation calculus (SC) is a formalism for reasoning about action. Within SC, the notion of state of a given situation is usually characterized by the set of fluents that hold in that situation. However, this concept is insufficient for system specification. To overcome this Limitation, an extension of SC is proposed, the situation and state calculus (SSC), where the concept of state is primitive, just like actions, situations and fluents. SSC is then compared with a branching temporal logic (BTL). A representation of BTL in SSC is defined and shown to establish a sound and complete encoding.
We present a dynamic form of observational logic for specifying concurrent systems on the basis of their observable behaviour, in particular without needing a language for describing states, which are regarded as non-...
详细信息
ISBN:
(纸本)3540662464
We present a dynamic form of observational logic for specifying concurrent systems on the basis of their observable behaviour, in particular without needing a language for describing states, which are regarded as non-observable. The logic is based on quantales. The models are labelled transition systems, and a weakly complete proof system is presented. We study the logic from the point of view of modularity;vertical modularity is based on a notion of implementation of systems and refinement of specifications, and horizontal modularity is based on parallel composition of systems and specifications. Several compositionality results are presented. As an example we see a specification of a stack and its implementation over an array and a pointer.
The proceedings contain 19 papers. The special focus in this conference is on programming Languages and Systems. The topics include: A decidable logic for describing linked data structures;interprocedural control flow...
ISBN:
(纸本)3540656995
The proceedings contain 19 papers. The special focus in this conference is on programming Languages and Systems. The topics include: A decidable logic for describing linked data structures;interprocedural control flow analysis;a per model of secure information flow in sequential programs;quotienting share for dependency analysis;types and subtypes for client-server interactions;types for safe locking;constructor subtyping;safe and principled language interoperation;deterministic expressions in C;a programminglogic for sequential java;set-based failure analysis for logic programs and concurrent constraint programs;simpler, and more expressive;type-based decompilation;an operational investigation of the CPS hierarchy;higher-order code splicing;expressing structural properties as language constructs;polytypic compact printing and parsing and dynamic programming via static incrementalization.
This study offers a characterization of the collection of properties expressible in Hennessy-Milner logic (HML) with recursion that can be tested using finite LTSs. In addition to actions used to probe the behaviour o...
详细信息
ISBN:
(纸本)3540657193
This study offers a characterization of the collection of properties expressible in Hennessy-Milner logic (HML) with recursion that can be tested using finite LTSs. In addition to actions used to probe the behaviour of the tested system, the LTSs that we use as tests will be able to perform a distinguished action nok to signal their dissatisfaction during the interaction with the tested process. A process a passes the test T iff T does not perform the action nok when it interacts with s. A test T tests for a property phi in HML with recursion iff it is passed by exactly the states that satisfy phi. The paper gives an expressive completeness result offering a characterization of the collection of properties ill HML with recursion that are testable in the above sense.
We develop an application of the reflective properties of rewriting logic to the specification of the management process of broadband telecommunications networks. The application is illustrated by a process that modif...
详细信息
ISBN:
(纸本)3540662464
We develop an application of the reflective properties of rewriting logic to the specification of the management process of broadband telecommunications networks. The application is illustrated by a process that modifies the demand of a service between two nodes in the network. The strategy language selected for controlling the process is based on the one presented in [2] which has been enhanced with a new operation that applies a strategy over a set of objects. The specification of the system is developed in the rewriting logic language Maude, which, thanks to its reflective capabilities, can also be used for specifying internally the strategies that control the system. Several modeling approaches are compared, emphasizing the benefits obtained from using reflection to control the rewriting process as opposed to the extra effort required to control the process at the object level itself.
We propose a definition of hierarchical heterogeneous formal specifications, where each module is specified according to its own homogeneous logic. We focus on the specification structure which we represent by a term ...
详细信息
ISBN:
(纸本)3540662464
We propose a definition of hierarchical heterogeneous formal specifications, where each module is specified according to its own homogeneous logic. We focus on the specification structure which we represent by a term in order to take benefit of classical knowledge on terms. For example, substitutions solve implementation sharing of modules. Then, we show how proof mechanisms can be expressed inside our framework. Our proof system involves both the homogeneous inference relations associated to the logics of modules and property inheritance relations associated to the structuring primitives. Heterogeneous primitives allow to move from one logic to another. We sketch out the specification of a travel agency given according to our particular framework of structured specifications. We demonstrate on this specification how a heterogeneous proof can be handled.
The proceedings contain 21 papers. The special focus in this conference is on Foundations of Software Science and Computation Structures. The topics include: An automata-theoretic approach to interprocedural data-flow...
ISBN:
(纸本)9783540657194
The proceedings contain 21 papers. The special focus in this conference is on Foundations of Software Science and Computation Structures. The topics include: An automata-theoretic approach to interprocedural data-flow analysis;reasoning about concurrent systems using types;a strong logicprogramming view for static embedded implications;unfolding and event structure semantics for graph grammars;an algebraic characterization of typability in ML with subtyping;the recognizability problem for tree automata with comparisons between brothers;categorical models of explicit substitutions;equational properties of mobile ambients;model checking logics for communicating sequential agents;a complete coinductive logical system for bisimulation equivalence on circular objects;string languages generated by total deterministic macro tree transducers;matching specifications for message sequence charts and probabilistic temporal logics via the modal Mu-calculus.
Tabled resolution improves efficiency as well as termination properties of logic programs by sharing answer computations across "similar" subgoals. Similarity based on subsumption of subgoals rather than var...
详细信息
暂无评论