| 1. |
- Ahlgren, Bengt, et al.
(författare)
-
A Host Interface to the DTM Network
- 1992. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- DTM, dynamic synchronous transfer mode, is a new time division multiplexing technique for fiber networks currently being developed and implemented at the Royal Institute of Technology in Stockholm, Sweden. This paper describes the hardware and software aspects of the design of an SBus host interface to the DTM network for a Sun SPARCstation. The interface is based on a dual port memory residing on the interface card and accesible over the SBus from the host CPU. The host operating system allocates message buffers directly in this memory. The interface has hardware support for segmenting and reassembling packets to and from the data units of the DTM. The software part of the interface manages the shared memory and the virtual circuits provided by the DTM network.
|
|
| 2. |
- Ali, Khayri Mohammed
(författare)
-
A method for implementing out in parallel execution of Prolog
- 1987. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- A method for implementing cut in parallel execution of Prolog is presented. It takes advantages of the efficient implementation of cut in the sequential WAM. It restricts the parallelism, however, it is simple and adds a small extra overhead over the sequential scheme. The method can be used in parallel execution of Prolog on shared amd nonshared memory multiprocessors.
|
|
| 3. |
- Ali, Khayri Mohammed, et al.
(författare)
-
An investigation of an OR parallel execution model for horn clause programs
- 1988. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a model for OR parallel execution of Horn clause programs on a combined local and shared memory multiprocessor system. In this model, the shared memory only contains control information that guides processors requesting a job to independently construct the environment required to get a new job. Each processor has a local memory containing its own binding environment. This reduces the traffic to the shared memory and allows each processor to process its job with high performance. Each processor is almost the same as Warren's Abstract Machine (WAM). A method for nonshared memory multiprocessor architectures is outlined. We also present some preliminary results of an experimental investigation of the model.
|
|
| 4. |
- Ali, Khayri Mohammed, et al.
(författare)
-
Global garbage collection for distributed heap storage systems
- 1987. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a garbage-collection algorithm, suitable for loosely-coupled multiprocessor systems, in which the processing elements (PE's) share only the communication medium. The algorithm is global, i.e. it involves all the PE's in the system. It allows space compaction, and it uses a system-wide marking phase to mark all accessible objects where a combination of parallel breadth-first/depth-first strategies is used for tracing the object-graphs according to a decentralized credit mechanism that regulates the number of garbage collection messages in the system. The credit mechanism is crucial for determining the space requirement of the garbage-collection messages. Also a variation of the above algorithm is presented for systems with high locality of reference. It allows each PE to perform first its local garbage collection and only invokes the global garbage collection when the freed space by the local collector is insufficient.
|
|
| 5. |
- Ali, Khayri Mohammed
(författare)
-
OR parallel execution of horn clause programs based on WAM and shared control information
- 1988. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- A method for OR parallel execution of Horn clause programs on a shared memory multiprocessor is presented. The shared memory contains only control information that guide processors requesting a job to independently construct the environment required to get a new job from the other processors without degrading the performance. Each processor has a local memory containing its own binding environment. This reduces the traffic to the shared memory and allows each processor to process its job with high performance. Each processor is almost the same as the Warren Abstract Machine (WAM). Modification to the WAM for supporting the method is described in detail. A method for nonshared memory multiprocessor architecture is outlined.
|
|
| 6. |
- Ali, Khayri Mohammed
(författare)
-
OR-Parallel Execution of Prolog on a Multi-Sequential Machine
- 1986. - 1
-
Rapport (refereegranskat)abstract
- Based on extending the sequential execution model of Prolog to include parallel execution, we present a method for OR-parallel execution of Prolog on a multiprocessor system. The method reduces the overhead incurred by parallel processing. It allows many processing elements (PEs) to process simultaneously a common branch of a search tree, and each of these PEs creates its local environment and selects a subtree for processing without communication. The run-time overhead is small: simple and efficient operations for selecting the proper subtree. Communication is necessary only when some PEs have exhausted their search spaces and there are others still searching for solutions. The method is able to utilize most of the technology devised for sequential implementation of Prolog. It is optimized for an architecture which supports broadcast copying.
|
|
| 7. |
- Ali, Khayri Mohammed
(författare)
-
OR parallel execution of Prolog on BC-machine
- 1988. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present the principles of OR-parallel execution of Prolog on a special parallel inference machine, named BC-machine. The machine is a combined local and shared memory multiprocessor with a special interconnection network. The network allows write operations of an active processor to be broadcasted to several idle processors simultaneously. The shared memory is mainly used for sharing some control information among processors in the system. The amount of shared control information is small and accessed relatively seldom. The execution model is based on the local address space approach. It allows all the technology developed for standard Prolog to be used without loss of efficiency. We expect that the model substantially reduces the copying overhead in comparision with all previous related models. This reduction is due to our new idea of dynamic load balancing and the broadcast mechanism supported by the network. A prototype system of 9 processors is under construction at the Swedish Institute of Computer Science in Stockholm.
|
|
| 8. |
- Ali, Khayri Mohammed, et al.
(författare)
-
Performance of Muse on Switch-Based Multiprocesor Machines
- 1992. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The Muse (multiple sequential Prolog engines) approach has been used to make a simple and efficient OR-parallel implementation of the full Prolog language. The performance results of the Muse system on bus-based multiprocessor machines have been presented in previous chapters, papers. This chapter paper discusses the implementation and performance results of the Muse system on switch-based multiprocessors (the BBN Butterfly GP1000 and TC2000). The results of Muse execution show that high real speedups can be achieved for Prolog programs that exhibit coarse-grained parallelism. The scheduling overhead is equivalent to around 8 -- 26 Prolog procedure calls per task on the TC2000. The chapter paper also compares the Muse results with corresponding results for the Aurora OR-parallel Prolog system. For a large set of benchmarks, the results are in favor of the Muse system.
|
|
| 9. |
- Ali, Khayri Mohammed, et al.
(författare)
-
The Engine-Scheduler Interface used in the Muse OR-parallel Prolog System
- 1992. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Almost any sequential Prolog system is in principle easy to extend for OR-parallelism, using the Muse execution model. To reduce your programming effort we have implemented the Muse scheduler, with a clean interface to the Prolog sequential engine. This interface is implemented as a set of C macros. The sequential Prolog system to be parallelized uses some of those macros provided by the Muse scheduler and must also provide some macros for the Muse scheduler. This chapter paper contains a definition and description of the required macros, emphasizing information needed by the Prolog engine programmer.
|
|
| 10. |
- Alshawi, Hiyan, et al.
(författare)
-
Bilingual conversation interpreter : a prototype interactive message translator. Final report
- 1991. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This document is the final report for a research project aimed at producing a prototype system for on-line translation of typed dialogues between speakers of different natural languages. The work was carried out jointly by SICS and SRI Cambridge. The resulting prototype system (called Billingual Conversation Interpreter, or BCI) translates between english and Swedish in both directions.The Major components of the BCI are two copies of the SRI Core Language Engine, equipped with English and Swedish grammars respectively. These are linked by the transfer and disambiguation components. Translation takes place by analyzing the source-language sentence into Quasi Logical Form ( QLF), a linguistically motivated logical representation, transferring this into a target-language QLF, and generating a target-language sentence. When ambiguities occur that cannot be resolved automatically, they are clarified by Querying the appropriate user. The clarification dialogue presupposes no knowledge of either linguistics or the other language. The prototype system has a broad grammatical coverage, a initial vocabulary of about 1000 words together with vocabulary expansion tools, and a set of English-Swedish transfer rules. The formalism developed for coding this linguistic information make it relatively easy to extend the system. We believe that the project was successful in demonstrating the feasibility of using these techniques for interactive translation applications, and provides a sound basis for development of a large scale message translator system with potential for commercial exploitation.The main sections of this report are the following: * A non-technical introduction, summarizing the BCI's design , and containing a sample session. * An overview of the Swedish version of the CLE. * A detailed discussion of the theory and practice of QLF transfer. * A description of the interactive disambiguation method. * Suggestions for possible follow-on projects aimed in the direction of practically usable commercial systems.
|
|
| 11. |
- Amadio, Roberto, et al.
(författare)
-
Reasoning about Higher-Order Processes
- 1994. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We address the specification and verification problem for process calculi such as Chocs, CML and Facile where processes or functions are transmissible values. Our work takes place in the context of a static treatment of restriction and of a bisimulation-based semantics. As a paradigmatic and simple case we concentrate on (Plain) Chocs. We show that Chocs bisimulation can be characterized by an extension of Hennessy-Milner logic including a constructive implication, or function space constructor. This result is a non-trivial extension of the classical characterization result for labelled transition systems. In the second part of the paper we address the problem of developing a proof system for the verification of process specifications. Building on previous work for CCS we present an infinitary sound and complete proof system for the fragment of the calculus not handling restriction.
|
|
| 12. |
- Andersson, Anders
(författare)
-
SAGA -- Syntax Analyzer Generator for Agents
- 1995. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- LALR(1) parser generators in conjunction with imperative programming languages is the standard solution for parsing applications. Contrary to popular belief, this situation is not entirely satisfactory. With imperative tools like Yacc, it is difficult to add actions to a grammar without introducing conflicts. Also, LALR(1) is not powerful enough to meet the needs of languages like C++. We argue that LALR(1) parsing in conjuction with concurrent constraint programming is an interesting option that solves the former problem. We also show how deep guards and don't-know non-determinism can be exploited to solve the latter problem. These ideas have been incorporated in the Saga parser generator described in this report. Saga is an integrated generator for lexical analyzers and parsers. It is based on AKL, a multiparadigm programming language based on a concurrent constraint framework. It is intended both as a research tool to demonstrate the power offered by concurrent constraints, and as a practical tool for the Agents programming system. As a practical tool, Saga features many improvements over tools like Yacc. For example, Saga offers powerful syntax, elegant reporting and resolution of conflicts and powerful error handling in the generated syntax analyzers.
|
|
| 13. |
- Appleby, Karen, et al.
(författare)
-
Garbage Collection for Prolog Based on WAM (Revised version)
- 1986. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Warren Abstract Machine (WAM) has become a generally accepted standard Prolog implementation technique. Garbage collection is an important aspect in the implementation of any Prolog system. We first present a synopsis of the WAM and then show marking and compaction algorithms that take advantage of WAM's unique use of the data areas. Marking and compaction are performed on both the heap and the trail. The marking and compaction algorithms use pointer reversal techniques, which obviate the need for extra stack space. However, two bits for every pointer on the heap are reserved for the garbage collection algorithm. The algorithm can work on segments of the heap, which may lead to a significant reduction of the total garbage collection time. The time of the algorithms are linear in the size of the areas.
|
|
| 14. |
- Aronsson, Martin
(författare)
-
A Definitional approach to the combination of functional and relational programming
- 1991. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We show how the programming language GCLA can be used to naturally express both relational and functional programs in an integrated framework. We give a short introduction to GCLA, and to the theory of partial inductive definitions on which GCLA is based. GCLA is best regarded as a logic programming language, but instead of saying that the query follows from the program in some a priori given logic, we say that the program defines the logic in which the query is proved. We then demonstrate how to implement both relational and functional programs as well as a combination of them in GCLA.
|
|
| 15. |
- Aronsson, Martin
(författare)
-
GAM: An abstract machine for GCLA
- 1989. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- GCLA is a new programming language, which increases expressiveness compared with traditional logic programming languages and functional programming languages. The basis for the language is a generalization of the concept inductive definitions, called partial inductive definitions. The program defines a logic, which is used to make inferences to prove if a query holds or not. This report first presents a short introduction to these ideas. Then, an abstract machine, called GAM, for GCLA is presented; the instructions as well as an introduction to the compiling schema is given together with some examples. The main idea is to extend the Warren Abstract Machine (WAM), which is an abstract machine for the language Prolog.
|
|
| 16. |
|
|
| 17. |
- Aronsson, Martin
(författare)
-
Implementational Issues in GCLA: A-Sufficiency and the Definiens Operation
- 1993. - 1
-
Rapport (refereegranskat)abstract
- We present algorithms for computing A-sufficient substitutions and constraint sets together with the definiens operation. These operations are primitive operations in the language GCLA. The paper first defines those primitives, which together form a dual rule to SLD resolution, and then describes the different algorithms and some of their properties together with examples. One of the algorithms shows how a definition can be compiled into a representation holding all possible A-sufficient substitutions/constraint sets together with their corresponding definiens. This representation makes the computation at runtime of a definiens and an A-sufficient substitution/constraint set have the same complexity as the table lookup operation clause/2 in Prolog. The paper also describes the generalisation from unification (sets of equalities) to constraint sets and satisfiability of systems of equalities and inequalities.
|
|
| 18. |
- Aronsson, Martin
(författare)
-
Implementational Issues in GCLA: Compiling Control
- 1993. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The paper describes the basic implementation of GCLA II's control level. The basis of the implementation is a compiling scheme for transforming inference rules and strategies operating on the object level to an interpreter in Prolog, where the inference rules of the control level are coded inline. This is possible since the operational semantics of the control level is deterministic, i.e. the choice of inference rule to apply on a control level goal is determined solely by the parts of the goal. To handle dynamic clauses, a context list, accessible through some new C-functions linked together with the Prolog system. GCLA I and GCLA II are described shortly, followed by a discussion of a Horn clause representation of inference rules versus functions coding inference rules. Then the transformation of inference rules and strategies is described followed by some examples.
|
|
| 19. |
- Aronsson, Martin
(författare)
-
Methodology and Programming Techniques in GCLA II
- 1992. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We will demonstrate various implementation techniques in the language GCLA. First an introduction to GCLA is given, followed by some examples of program developments, to demonstrate the development methodology. Other examples are also given to show various implementation techniques and properties of the system.
|
|
| 20. |
- Aronsson, Martin
(författare)
-
Planning the Construction of a Building
- 1993. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The paper describes a tool for generating plans for the construction of a building. The application is implemented in GCLA, together with a simple constraint solving system. The main idea is that experiences from other plans are stored in methods; which are a systematic way of grouping activities together as higher level activities that can solve more complex tasks. Activities are entities that perform some action on a model of the real world, called the global state. Activities have preconditions, i.e. starting conditions, some representation of time and resource consumption, and postconditions, i.e. how and what to change in the global state. Scheduling activities amounts to allocating resources and placing the activities in time. The goal of the planning process, i.e what we want the planning process to achieve, is represented by a geometric model of the changed global state, i.e. a design of the specified building that one wants to build. To create plans, the system is divided into two main phases; the choice-of-method phase and the scheduling phase. In the choice-of-method phase suitable methods are chosen based on experience from the past. Such methods already exists in the building industry, although not in an explicit formal representation. Then the scheduling phase allocates resources and places the activities in time by reasoning about the activities' change of the global state. The goal of the planning process is that the objects of the specified design should be produced and represented in the global state. The user can change most of the behaviour of the system by indicating what he wants it to do. He can change activities, their preconditions, calculations and postconditions, he can change methods, or add or remove activities to them, he can change resources etc. By this flexibility, the user can form his system to reflect his own preferences about how to plan and what to plan.
|
|
| 21. |
- Aronsson, Martin
(författare)
-
STRIPS-Like planning using GCLA
- 1989. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This report describes how a STRIPS planning system can be implemented in GCLA. A short introduction to the problem of the blocks world is given, as well as an introduction to STRIPS. Then the GCLA program implementing the planning system is presented, together with queries concerning planning and simulation problems.
|
|
| 22. |
- Aronsson, Martin, et al.
(författare)
-
The programming language GCLA: A definitional approach to logic programming
- 1989. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a logic programming language, GCLA (Generalized horn Clause LAnguage), that is based on a generalization of Prolog. This generalization is unusual in that it takes a quite different view of the meaning of a logic program--a "definitional" view rather than the traditional logical view. GCLA has a number of noteworthy properties, for instance hypothetical and non-monotonic reasoning. This makes implementation of reasoning in knowledge-based systems more direct in GCLA than in Prolog. GCLA is also general enough to incorporate functional programming as a special case. GCLA and its syntax and semantics are described. The use of various language constructs are illustrated with several examples.
|
|
| 23. |
- Backlund, Björn, et al.
(författare)
-
A graphical G-LOTOS editor defined by meta-tool LOGGIE
- 1989. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a prototype implementation of a graphical editor for a subset of G-LOTOS. The graphical G-LOTOS syntax is beeing standardized within ISO for the LOTOS specification language. First, we provide a formal definition of the G-LOTOS subset. Then, the specification the editor is derived from this formal definition. Finally, the editor is generated automatically using the LOGGIE meta-tool.
|
|
| 24. |
- Backlund, Björn, et al.
(författare)
-
Generation of graphic language-oriented design environments
- 1989. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We review some results in the area of using meta techniques to generate language-oriented programming environments. We focus on environments for languages having a two-dimensional syntax based on attribute grammars and constraints. We introduce edit-semantic attributes, a new classof attributes which control the user interaction and graphic presentation. We present LOGGIE, a prototype tool implementing some of the meta techniques discussed. The tool generates interactive language-oriented graphical editors.
|
|
| 25. |
- Bretan, Ivan
(författare)
-
Natural Language in Model World Interfaces
- 1995. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- An essay on rationale and methodology of combining natural language and other means of interaction in multimodal interfaces.
|
|
| 26. |
- Bretan, Ivan, et al.
(författare)
-
Synergy Effects in Natural Language-Based Multimodal Interaction
- 1994. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We discuss the synergetic effects that can be obtained in an integrated multimodal interface framework comprising on one hand a visual language-based modality and on the other natural language analysis and generation components. Besides a visual language with high expressive power, the framework includes a cross-modal translation mechanism which enables mutual illumination of interface language syntax and semantics. Special attention has been payed to how to address problems with robustness and pragmatics through unconventional methods which aim to enable user control of the discourse management process.
|
|
| 27. |
- Brown, Charles Grant, et al.
(författare)
-
Action-Tracking in DIVE
- 1994. - 1
-
Rapport (refereegranskat)abstract
- Several approaches to intelligent tutoring monitor the learners actions in order to understand his/her abilities. This requires that the learner's actions can be monitored. In traditional single-user command interfaces this is straightforward. As a result action tracking has not been subject to much study. However, in more advanced interfaces and applications, it is no longer self-evident how action tracking should be done, or even what should be considered an action. This paper addresses two particular aspects of systems of today that make action tracking hard: The increasing naturalness of interfaces, and the introduction of environments for human collaboration. The DIVE environment is extremely advanced in both these aspects, being a virtual reality environment for unconstrained human collaboration. We characterize the possibilities and limitations for action tracking in DIVE, and suggest an architecture for the task.
|
|
| 28. |
- Carlsson, Mats
(författare)
-
A Prolog compiler and its extension for OR-parallelism
- 1990. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This report describes algorithms for the compiler component of the Aurora Or-Parallel Prolog system. The compiler translates one Prolog clause at a time into a sequence of abstract instructions. The instruction set is based on the sequential Warren Ab- stract Machine (WAM) with extensions for full Prolog, shallow backtracking, memory management and garbage collection, and for the SRI model of or-parallel execution of Prolog. Most of the described algorithms apply to compilation of sequential Prolog programs. The extensions introduced to support or-parallelism are minor, and concern pruning operators (cut and commit) and compile-time allocation of binding array offsets for permanent variables (generalised environment trimming). Code generation proper is kept separate from register allocation, and uses heuristics for finding a compilation order which minimises the number of register-register copies. After such copies have been coalesced where possible, register allocation is performed in a single pass over the intermediate code. The various compilation phases are described in detail, and the implementation is compared with some other compilers.
|
|
| 29. |
|
|
| 30. |
- Carlsson, Mats
(författare)
-
Freeze, indexing, and other implementation issues in the WAM
- 1986. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Two very useful extensions to Prolog's computation model, dif and freeze were introduced with Prolog II. A method for their incorporation into the Warren Abstract Machine is presented. Under reasonable assumptions, the method does not incur any overhead on programs not using these extensions. The clause indexing mechanism is also discussed, as it is not unrelated to the freeze mechanism.
|
|
| 31. |
- Carlsson, Mats
(författare)
-
On the Efficiency of Optimising Shallow Backtracking in Prolog
- 1990. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The cost of backtracking has been identified as one of the bottlenecks in achieving peak performance in compiled Prolog programs. Much of the backtracking in Prolog programs is shallow, i.e. is caused by unification failures in the head of a clause when there are more alternatives for the same procedure, and so special treatment of this form of backtracking has been proposed as a significant optimisation. This paper describes a modified WAM which optimises shallow backtracking. Four different implementation approaches are compared. A number of benchmark results are presented, measuring the relative tradeoffs between compilation time, code size, and run time. The results show that the speedup gained by this optimisation can be significant.
|
|
| 32. |
|
|
| 33. |
- Carlsson, Mats, et al.
(författare)
-
The Aurora Abstract Machine and its Emulator
- 1990. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Aurora is a prototype Or-Parallel implementation of the full Prolog language fot shared-memory multiprocessors, developed as part of an informal research collaboration known as the "Gigalips Project". This report describes the abstract machine of the implementation, expressed in terms of a Prolog engine adapted for Or-Parallel execution by means of the SRI model. An algorithms interface defining the communication between the engine and sheduler components of each Aurora process is described, and enables different engine and scheduler components to be used interchangeably. Both the interface and the engine are Fundamentally revised versions of those used in previous generations of the implementation.
|
|
| 34. |
- Ciepielewski, Andrzej, et al.
(författare)
-
Performance evaluation of a storage model for OR-parallel execution of logic programs
- 1986. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- As the next step towards a computer architecture for parallel execution of logic programs we have implemented four refinements of the basic storage model for OR-Parallelism and gathered data about their performance on two types of shared memory architectures, with and without local memories. The results show how the different properties of the implementations influence performance, and indicate that the implementations using hashing techniques (hash windows) will perform best, especially on systems with a global storage and caches. We rise the question of the usefulness of the simulation technique as a tool in developing new computer architectures. Our answer is that simulations can not give the ultimate answers to the design questions, but if only the judiciosly chosen parts of the machine are simulated on a detailed level, then the obtained results can give a very good guidance in making design choice.
|
|
| 35. |
- Cleaveland, Rance, et al.
(författare)
-
The concurrency workbench: A semantics based tool for the verification of concurrent systems
- 1991. - 1
-
Rapport (refereegranskat)abstract
- The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key features is its breadht: a variety of different verification methods, including equivalence checking, preorder checking, and model checking, are supported for several different process semantics. One experience from our work is that a large number of interesting verification methods can be formulated as combinations of a small number of primitive algorithms. The Workbench has been applied to the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research.
|
|
| 36. |
- Dam, Mads
(författare)
-
Model Checking Mobile Processes (Full version)
- 1994. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We introduce a temporal logic for the polyadic pi-calculus based on fixed point extensions of Hennessy-Milner logic. Features are added to account for parametrisation, generation, and passing of names, including the use, following Milner, of dependent sum and product to account for (unlocalised) input and output, and explicit parametrisation on names using lambda-abstraction and application. The latter provides a single name binding mechanism supporting all parametrisation needed. A proof system and decision procedure is developed based on Stirling and Walker's approach to model checking the modal mu-calculus using constants. One difficulty, for both conceptual and efficiency-based reasons, is to avoid the explicit use of the omega-rule for parametrised processes. A key idea, following Hennessy and Lin's approach to deciding bisimulation for certain types of value-passing processes, is the relativisation of correctness assertions to conditions on names. Based on this idea a proof system and decision procedure is obtained for arbitrary pi-calculus processes with finite control, pi-calculus correlates of CCS finite-state processes, avoiding the use of parallel composition in recursively defined processes.
|
|
| 37. |
- Dam, Mads
(författare)
-
On Adaptable Support for Cooperative Work
- 1994. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- A critical dimension in the handling of change in computer-based systems for cooperative work is whether mechanisms for change should be explicitly embedded into systems, or whether change should be handled in a global and uniform manner, for instance by a process of editing and recompiling programs or scripts on the fly. We argue that to reflect the structure of organisations, powers of change must be local, structured, and dynamic. Thus a global and uniform handling of change is in general insufficient. We propose a formal basis for the description of dynamically modifiable objects, and explore its applicability in the field of CSCW by exposing it to three examples of increasing complexity: A system for dynamic communication channel creation; an adaptable conversation manager; and a rudimentary, yet quite general, awareness model.
|
|
| 38. |
- Dam, Mads
(författare)
-
On the Decidability of Process Equivalences for the pi-calculus
- 1994. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present general results for showing process equivalences applied to the finite control fragment of the pi-calculus decidable. Firstly a Finite Reachability Theorem states that up to finite name spaces and up to a static normalisation procedure, the set of reachable agent expressions is finite. Secondly a Boundedness Lemma shows that no potential computations are missed when name spaces are chosen large enough, but finite. We show how these results lead to decidability for a number of pi-calculus equivalences such as strong or weak, late or early bismulation equivalence. Furthermore, for strong late equivalence we show how our techniques can be used to adapt the well-known Paige-Tarjan algorithm. Strikingly this results in a single exponential running time not much worse than the running time for the case of for instance CCS. Our results considerably strengthens previous results on decidable equivalences for parameter-passing process calculi.
|
|
| 39. |
- Dam, Mads, et al.
(författare)
-
On the Verification of Open Distributed Systems
- 1997. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- A logic and proof system is introduced for specifying and proving properties of open distributed systems. Key problems that are addressed include the verification of process networks with a changing interconnection structure, and where new processes can be continuously spawned. To demonstrate the results in a realistic setting we consider a core fragment of the Erlang programming language. Roughly this amounts to a first-order actor language with data types, buffered asynchronous communication, and dynamic process spawning. Our aim is to verify quite general properties of programs in this fragment. The specification logic extends the first-order $\mu$-calculus with Erlang-specific primitives. For verification we use an approach which combines local model checking with facilities for compositional verification. We give a specification and verification example based on a billing agent which controls and charges for user access to a given resource.
|
|
| 40. |
- Eineborg, Martin, et al.
(författare)
-
Neural Networks for Wordform Recognition
- 1994. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The paper outlines a method for automatic lexical acquisition using three-layered back-propagation networks. Several experiments have been carried out where the performance of different network architectures have been compared to each other on two tasks: overall part-of-speech (noun, adjective or verb) classification and classification by a set of 13 possible output categories. The best results for the simple task were obtained by networks consisting of 204-212 input neurons and 40 hidden-layer neurons, reaching a classification rate of 93.6%. The best result for the more complex task was 96.4%, which was achieved by a net with 423 input neurons and 80 hidden-layer neurons. These results are rather promising and the paper compares them to the performance reported by rule-based and purely statistical methods; a comparison that shows the neural network completely compatible with the statistical approach. The rule-based method is, however, still better, even though it should noted that the task that the rule-based system performs is somewhat different from that of the neural net.
|
|
| 41. |
- Elshiewy, Nabiel A.
(författare)
-
Time, clocks and committed choice parallelism for logic programming of real time computations
- 1986. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- A model for logic programming of real time computing systems is presented. The model is based on the process interpretation of Horn-Clause Logic and employs a non-deterministic committed-choice stream-And parallel search strategy. A real time computing system is represented as a network of communicating goals where each goal maintains its own logical clock which can be read and set by the node reduction process. The system of distributed logical clocks satisfies Lamport's correctness and distributed synchronisation conditions. The programming language is a variant of GHC to which many features are borrowed from PARLOG. Primitives to express time and timing constraints are provided. A meta-interpreter is given to describe the operational semantics of the language and the implementability of the model in the language itself. A telecommunications switching system has been specified and implemented in terms of the model presented here. It is also shown that the fairness problem has a natural solution in the proposed logical frame work. This is illustrated through a real time fair binary merge operator.
|
|
| 42. |
- Eriksson, Lars-Henrik
(författare)
-
A finitary version of the calculus of partial inductive definitions
- 1992. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The theory of partial inductive definitions is a mathematical formalism which has proved to be useful in a number of different applications. The fundamentals of the theory is shortly described. Partial inductive definitions and their associated calculi are essentially infinitary. To implement them on a computer, they must be given a formal finitary representation. We present such a finitary representation, and prove its soundness. The finitary representation is given in a form with and without variables. Without variables, derivations are unchanging entities. With variables, derivations can contain logical variables that can become bound by a binding environment that is extended as the derivation is constructed. The variant with variables is essentially a generalization of the pure GCLA programming language.
|
|
| 43. |
- Eriksson, Lars-Henrik, et al.
(författare)
-
A programming calculus based on partial inductive definitions (with an introduction to the theory of partial inductive definitions)
- 1988. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We present a general framework (a programming calculus) for the specification, verification and synthesis of programs. The underlying programming paradigm is similar in spirit to logic programming but based on the theory of partial inductive definitions instead of predicate logic. Within this framework we give criteria for the correctness of programs and outline a methodology for using these criteria to perform verifications and syntheses. The programming calculus permits us to use an arbitrary specification language, as long as this language itself can be defined within our framework. The program language is based on partial inductive definitions. Such definitions can be regarded as sets of an extension to Horn clauses of logic, so traditional logic (pure Prolog) programs are included as a special case. Since the theory of partial inductive definitions is not widely known, we include an introduction to it. This introduction can also be read by itself, without any interest in the programming calculus.
|
|
| 44. |
- Eriksson, Lars-Henrik, et al.
(författare)
-
Formal specification and validation of a cache-coherence protocol
- 1995. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We specify a cache coherence protocol for cache-only shared memory multiprocessor architectures using the $\pi$-calculus. The analysis of the specification of the protocol is discussed, with emphasis on the use of the modal $\mu$-calculus to express correctness properties. The protocol specification is expressed using recursion variables inside parallel composition and thus it does not adhere to the syntactic requirements for finite control. We argue that the specification still belongs to a class of $\pi$-calculus processes for which model checking and bisimilarity checking is decidable. The relaxation of the syntactical requirement for finite control permits more natural specifications to be made. We expect that specifications which are naturally expressed using recursion variables inside parallel compositions but still permit decidable analyses are common in practise.
|
|
| 45. |
- Falkman, Göran, et al.
(författare)
-
Technical Diagnosis of Telecommunication Equipment - An Implementation of a Task specific Problems solving method (TDFL) using GCLA II
- 1993. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- This paper describes an implementation of a small knowledge-based system in GCLA II. GCLA II is perhaps best described as a logical programming language, with some properties usually found among functional languages, and it includes hypothetical and non-monotonic reasoning as integral parts, which makes it easy to handle hypothetical queries, negation and AI-techniques like simulation and planning in a natural way. It also makes implementation of reasoning in knowledge-based systems (KBS) more direct than in Prolog. The application is an already existing KBS that guides a service technician in the task of diagnosing a specific device which is a measuring instrument for testing telecommunications equipment. The method used in the application is a problem solving method called TDFL. The TDFL method is a task specific problem solving method for technical diagnosis that gives strong support for knowledge acquisition. The method is adapted to cope with some features of the application. For example, it gives support for reducing the time required for observations and it handles parts that are not directly testable. This paper describes how to adjust the TDFL method to remedy some errors present in the original version; avoiding unnecessary search of the device and eliminating unnecessary confirmations. Some future extensions to both the TDFL method and the implementation are also presented; allowing the search for more than one fault and the possibility of turning the diagnosis backwards.
|
|
| 46. |
- Franzén, Torkel
(författare)
-
Algorithmic aspects of intuitionistic propositional logic
- 1987. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- An algorithm for deciding validity in the intuitionistic propositional calculus is presented, together with source code in Quintus Prolog and some test data. The algorithm is based on an analysis of the use of contraction in the intuitionistic propositional sequent calculus, and also includes the techniques of "or-locking", "implication gathering", and "irrelevance checking".
|
|
| 47. |
- Franzén, Torkel
(författare)
-
Algorithmic aspects of intuitionistic propositional logic II
- 1989. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- In this report, a decision procedure for intuitionistic propositional logic is presented which is an improvement of the procedure presented in SICS report R87010B, "Algorithmic Aspects of Intuitionistic Propositional Logic," and its completeness proved. Also, a set of benchmarks is presented together with the results obtained from a parallel implementation of the algorithm.
|
|
| 48. |
|
|
| 49. |
- Franzén, Torkel
(författare)
-
Logic programming and the intuitionistic sequent calculus
- 1988. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The report contains some basic logical results and observations relevant to the use of intuitionistic logic as a programming language. In particular, a Kripke completeness proof is given for a formalization of intuitionistic logic incorporating quasi-free identity, and it is argued that full intuitionistic logic is too complicated to be useful, in spite of its superficial "constructive" aspects.
|
|
| 50. |
- Franzén, Torkel
(författare)
-
Logical aspects of the Andorra Kernal Language
- 1991. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- The Computation model for Kernal Andorra is Presented, and some logical aspects treated. In particular a soundness theorem relative to a modified completion involving a logical interpretation of cut procedures is proved, together with a completeness theorem for wait-clauses.
|
|
