Search

• < Previous
• 1
• Next >

---

Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Lei Song ; Lijun Zhang ; Jens Chr. Godskesen ; Flemming Nielson.

Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its&nbsp;[&hellip;]

---

A Coordination Language for Databases

Ximeng Li ; Xi Wu ; Alberto Lluch Lafuente ; Flemming Nielson ; Hanne Riis Nielson.

We present a coordination language for the modeling of distributed database applications. The language, baptized Klaim-DB, borrows the concepts of localities and nets of the coordination language Klaim but re-incarnates the tuple spaces of Klaim as databases. It provides high-level abstractions and&nbsp;[&hellip;]

---

Efficient CSL Model Checking Using Stratification

Lijun Zhang ; David N. Jansen ; Flemming Nielson ; Holger Hermanns.

For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approximation algorithm with worse than exponential&nbsp;[&hellip;]

---

Discovering, quantifying, and displaying attacks

Roberto Vigo ; Flemming Nielson ; Hanne Riis Nielson.

In the design of software and cyber-physical systems, security is often perceived as a qualitative need, but can only be attained quantitatively. Especially when distributed components are involved, it is hard to predict and confront all possible attacks. A main challenge in the development of&nbsp;[&hellip;]

---