| 1. |
- Abdulla, Parosh Aziz, et al.
(author)
-
A general approach to partial order reductions in symbolic verification
- 1998
-
In: Computer Aided Verification. - 9783540646082 - 9783540693390 ; , s. 379-390
-
Conference paper (peer-reviewed)abstract
- The purpose of partial-order reduction techniques is to avoid exploring several interleavings of independent transitions when model checking the temporal properties of a concurrent system. The purpose of symbolic verification techniques is to perform basic manipulations on sets of states rather than on individual states. We present a general method for applying partial order reductions to improve symbolic verification. The method is equally applicable to the verification of finite-state and infinite-state systems. It considers methods that check safety properties, either by forward reachability analysis or by backward reachability analysis. We base the method on the concept of commutativity (in one direction) between predicate transformers. Since the commutativity relation is not necessarily symmetric, this generalizes those existing approaches to partial order verification which are based on a symmetric dependency relation.We show how our method can be applied to several models of infinite-state systems: systems communicating over unbounded lossy FIFO channels, and unsafe (infinite-state Petri Nets. We show by a simple example how partial order reduction can significantly speed up symbolic backward analysis of Petri Nets.
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(author)
-
On-the-fly analysis of systems with unbounded, lossy FIFO channels
- 1998
-
In: Computer Aided Verification. - 9783540646082 - 9783540693390 ; , s. 305-318
-
Conference paper (peer-reviewed)abstract
- We consider symbolic on-the-fly verification methods for systems of finite-state machines that communicate by exchanging messages via unbounded and lossy FIFO queues. We propose a novel representation formalism, called simple regular expressions (SREs), for representing sets of states of protocols with lossy FIFO channels. We show that the class of languages representable by SREs is exactly the class of downward closed languages that arise in the analysis of such protocols. We give methods for (i) computing inclusion between SREs, (ii) an SRE representing the set of states reachable by executing a single transition in a system, and (iii) an SRE representing the set of states reachable by an arbitrary number of executions of a control loop of a program. All these operations are rather simple and can be carried out in polynomial time. With these techniques, one can construct a semi-algorithm which explores the set of reachable states of a protocol, in order to check various safety properties.
|
|
| 3. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Undecidable verification problems for programs with unreliable channels
- 1996
-
In: Automata, Languages and Programming. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540582014 - 9783540485667 ; , s. 71-90
-
Conference paper (peer-reviewed)abstract
- We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model e.g. link protocols such as the Alternating Bit Protocol and HDLC. In an earlier paper, we showed that several interesting verification problems are decidable for this class of systems, namely (1) the reachability problem: is a set of states reachable from some other state of the system, (2) safety property over traces formulated as regular sets of allowed finite traces, and (3) eventuality properties: do all computations of a system eventually reach a given set of states. In this paper, we show that the following problems are undecidable, namelyThe model checking problem in propositional temporal logics such as Propositional Linear Time Logic (PTL) and Computation Tree Logic (CTL).The problem of deciding eventuality properties with fair channels: do all computations eventually reach a given set of states if the unreliable channels are fair in the sense that they deliver infinitely many messages if infinitely many messages are transmitted. This problem can model the question of whether a link protocol, such as HDLC, will eventually reliably transfer messages across a medium that is not permanently broken.The results are obtained through a reduction from a variant of Post's Correspondence Problem.
|
|
| 4. |
- Abdulla, Parosh Aziz, et al.
(author)
-
Verifying networks of timed processes
- 1998
-
In: Tools and Algorithms for the Construction and Analysis of Systems. - 9783540643562 - 9783540697534 ; , s. 298-312
-
Conference paper (peer-reviewed)abstract
- Over the last years there has been an increasing research effort directed towards the automatic verification of infinite state systems, such as timed automata, hybrid automata, data-independent systems, relational automata, Petri nets, and lossy channel systems. We present a method for deciding reachability properties of networks of timed processes. Such a network consists of an arbitrary set of identical timed automata, each with a single real-valued clock. Using a standard reduction from safety properties to reachability properties, we can use our algorithm to decide general safety properties of timed networks. To our knowledge, this is the first decidability result concerning verification of systems that are infinite-state in “two dimensions”: they contain an arbitrary set of (identical) processes, and they use infinite data-structures, viz. real-valued clocks. We illustrate our method by showing how it can be used to automatically verify Fischer's protocol, a timer-based protocol for enforcing mutual exclusion among an arbitrary number of processes.
|
|
| 5. |
|
|
| 6. |
- Aronsson, Göran, et al.
(author)
-
Remarkably slow folding of a small protein.
- 1997
-
In: FEBS Letters. - 0014-5793 .- 1873-3468. ; 411:2-3, s. 359-364
-
Journal article (peer-reviewed)abstract
- Equilibrium denaturation of the 72 amino acid alpha/beta-protein MerP, by acid, guanidine hydrochloride, or temperature, is fully reversible and follows a two-state model in which only the native and unfolded states are populated. A cis-trans equilibrium around a proline peptide bond causes a heterogeneity of the unfolded state and gives rise to a slow- and a fast folding population. With a rate constant of 1.2 s(-1) for the major fast folding population, which has none of the common intrinsically slow steps, MerP is the slowest folding protein of this small size yet reported.
|
|
| 7. |
|
|
| 8. |
- Carlsson, Christina, 1968, et al.
(author)
-
Dancing DNA in Capillary Solution Electrophoresis
- 1995
-
In: Journal of the American Chemical Society. - : American Chemical Society (ACS). - 1520-5126 .- 0002-7863. ; 117:13, s. 3871-3872
-
Journal article (peer-reviewed)
|
|
| 9. |
- Carlsson, Christina, 1968, et al.
(author)
-
OPTICAL AND PHOTOPHYSICAL PROPERTIES OF THE OXAZOLE YELLOW DNA PROBES YO AND YOYO
- 1994
-
In: Journal of Physical Chemistry. - : American Chemical Society (ACS). - 0022-3654 .- 1541-5740. ; 98:40, s. 10313-10321
-
Journal article (peer-reviewed)abstract
- The photophysical properties of the optical DNA probe YOYO (homodimeric derivative of oxazole yellow) have been characterized in terms of the monomeric part, the YO chromophore. In aqueous solutions YO is virtually nonfluorescent but upon binding to DNA its fluorescence quantum yield is strongly increased. A similar enhancement of the fluorescence is observed for YO in the viscous solvent glycerol. The high fluorescence quantum yield of YO, when bound to DNA or in a viscous solution, is proposed to be a result of decreased rotational mobility around the internuclear bridge between the two aromatic ring systems. This hypothesis is based on similar values of the activation energies for the temperature-dependent nonradiative decay processes (E(A) = 53 kJ/mol) and viscous flow (E(A) = 63 kJ/mol), suggesting related rate-limiting mechanisms. A single electronic transition is found to be responsible for the intense visible absorption band. This conclusion is based on the observation of an essentially wavelength-independent reduced linear dichroism and similarly wavelength independent fluorescence anisotropy, and the fact that the emission spectrum is very nearly a mirror image of the absorption spectrum. The conclusion is further supported by quantum mechanical calculations (CNDO/S). By combination of measurements of fluorescence anisotropy of YO in glycerol and linear dichroism of YO in a stretched poly(vinyl alcohol) film, the transition moment of the strong visible absorption band was found to be nearly long axis polarized, in agreement with the CNDO/S calculations. The low-energy electronic transition and its polarization direction in the YO chromophore remain essentially unperturbed in the YOYO dye, suggesting that the results obtained for the excited state of the YO chromophore are applicable also to YOYO. One difference, though, is that in aqueous solutions the two YO chromophores of YOYO interact with each other, forming an internal dimer, resulting in a distorted absorption spectrum.
|
|
| 10. |
- Carlsson, Christina, 1968, et al.
(author)
-
Screening for genetic mutations
- 1996
-
In: Nature. - : Springer Science and Business Media LLC. - 0028-0836 .- 1476-4687. ; 380:6571, s. 207-
-
Journal article (other academic/artistic)
|
|
