| 1. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
An Introduction to Symbolic Trajectory Evaluation
- 2006
-
Ingår i: Lecture notes of the sixth International School on Formal Methods for the Design of Computer, Communication and Software Systems: Hardware Verification, Lecture Notes in Computer Science. ; 3965
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)
|
|
| 2. |
|
|
| 3. |
- Roorda, Jan-Willem, 1975, et al.
(författare)
-
A new SAT-based Algorithm for Symbolic Trajectory Evaluation
- 2005
-
Ingår i: Proceedings of Correct Hardware Design and Verification Methods 2005, (CHARME 2005). - 3540291059 ; 3725, s. 238-253
-
Konferensbidrag (refereegranskat)abstract
- We present a new SAT-based algorithm for Symbolic Trajectory Evaluation (STE), and compare it to more established SAT-based techniques for STE.
|
|
| 4. |
|
|
| 5. |
|
|
| 6. |
- Roorda, Jan-Willem, 1975, et al.
(författare)
-
Iterated Belief Change in Multi Agent Systems
- 2003
-
Ingår i: Logic Journal of the IGPL. - : Oxford University Press (OUP). - 1367-0751 .- 1368-9894. ; 11:2, s. 223-246
-
Tidskriftsartikel (refereegranskat)abstract
- We give a model for iterated belief change in multi-agent systems. The formal tool we use for this is a combination of modal and dynamic logic. Two core notions in our model are the expansion of the knowledge and beliefs of an agent, and the processing of new information. An expansion is defined as the change in the knowledge and beliefs of an agent when it decides to believe an incoming formula while holding on to its current propositional beliefs. To prevent our agents from forming inconsistent beliefs they do not expand with every piece of information they receive. Instead, our agents remember their original beliefs and every piece of information they receive. After every receipt of information they decide which (consistent) subset of the received information should be incorporated into their original beliefs. This procedure is called the processing of new information. We show that our model of belief update behaves in an intuitive way and that it is not sensitive to criticism on comparable models.
|
|
| 7. |
- Roorda, Jan-Willem, 1975, et al.
(författare)
-
Iterated belief change in multi-agent systems
- 2002
-
Ingår i: Proceedings of the 1st International Joint Conference on: Autonomous Agents adn Multiagent Systems, Bologna, 15-19 July 2002. - New York, New York, USA : ACM Press. - 1581134800 ; , s. 889-896
-
Konferensbidrag (refereegranskat)abstract
- We give a model for iterated belief change in multi-agent systems. The formal tool we use for this is a combination of modal and dynamic logic. Two core notions in our model are the expansion of the knowledge and beliefs of an agent, and the processing of new information. An expansion has been defined as the change in the knowledge and beliefs of an agent when it decides to believe an incoming formula while holding on to its current propositional beliefs. To prevent our agents from forming inconsistent beliefs they do not expand with every piece of information they receive. Instead, our agents remember their original beliefs and every piece of information they receive. After every receipt of information they decide which (consistent) subset of the received information should be incorporated into their original beliefs. This procedure is called the processing of new information. We show that our model of belief update behaves in an intuitive way and that it is not sensitive to criticism on comparable models.
|
|
| 8. |
- Roorda, Jan-Willem, 1975
(författare)
-
Semantics, Decision Procedures, and Abstraction Refinement for Symbolic Trajectory Evaluation
- 2006
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- The rapid growth in hardware complexity has led to a need for formal verification of hardware designs to prevent bugs from entering the final silicon. Model-checking is a verification method in which a model of a system is checked against a property, describing the desired behaviour of the system over time. Today, all major hardware companies use model-checkers in order to reduce the number of bugs in their designs.Symbolic Trajectory Evaluation (STE) is a model-checking technique for hardware. STE uses abstraction, meaning that details of the circuit behaviour are removed from the circuit model. This improves the capacity limits of the method, but has as down-side that certain properties cannot be proved if the wrong abstraction is chosen. STE is limited to properties ranging over a finite numberof time-steps. Generalised Symbolic Trajectory Evaluation (GSTE) is an extension of STE that can deal with properties ranging over unbounded time.This thesis describes several important contributions to research on STE and GSTE.First of all, the thesis describes a SAT-based method for abstraction refinement in STE. A main drawback of STE is that the user needs to spend time on finding the right abstraction. Often, a great deal of time is spent on such manual abstraction refinement.To address this problem, we have invented a method for assisting STE users with manual abstraction refinement. As a case study, we have demonstrated the usefulness of the algorithm by showing how to refine and verify an STE specification of a Content-Addressable Memory (CAM).Furthermore, the thesis describes faithful semantics for STE and GSTE.The reason for developing these semantics is that we have discovered thatthe existing semantics for STE and GSTE do not correspond to the proving power of the corresponding model-checking algorithms.We believe that the semantics are an important contribution for at least two reasons. First of all, a faithful semantics makes STE and GSTE more accessible to novice users: a faithful semantics enables users to understand the abstraction used in STE and GSTE, without having to understand the details of the model-checking algorithm.Secondly, a faithful semantics can be used as basis for research on new model-checking algorithms and other tools for STE and GSTE.To illustrate this, building upon our faithful semantics for STE, we have developed the third contribution of this thesis: a new SAT-based model-checking algorithm for STE. In the thesis, we demonstrate on a series of benchmarks that our new algorithm outperforms other SAT-based model-checking algorithms for STE.
|
|
| 9. |
|
|
