TUD Logo

TUD Home » ... » Theoretical Computer Science » Chair of Algebraic and Logical Foundations of Computer Science » Projects

Chair of Algebraic and Logical Foundations of Computer Science

Current third-party funded projects:

RoSI

DFG Research Training Group "Role-based Software Infrastructures for Continuous-Context-Sensitive Systems"

QuantLA

DFG Research Training Group "Quantitative Logics and Automata"

HAEC

Collaborative Research Centre SFB912 "Highly Adaptive Energy-Efficient Computing"

cfaed

Center for Advancing Electronics Dresden

CeTI

Centre for Tactile Internet with Human-in-the-Loop

DFG-Projekt BA-1679/11-1

The project "Modellprüfung für temporale Logiken und gewichtete probabilistische Strukturen" considers theoretical aspects of combining assertions on accumulated weights with temporal logics.

DFG-Projekt BA-1679/12-1

The project "Nicht-Mehrdeutigkeit, Alternierung und Nichtstandardakzeptanz in automatenbasierter Modellprüfung probabilistischer Systeme" considers theoretical and practical aspects of various automata-based approaches to probabilistic model checking for linear temporal logics.

5G Lab Germany



Former third-party funded projects:

SREX

Secure Remote EXecution

IMData

Integrated Hard- and Software Mechanisms for Data-intensive Applications on Heterogeneous Manycore Systems

MEALS

Mobility between Europe and Argentina applying Logics to Systems

QuaOS

The scientific goal of the DFG-project QuaOS was research on methods and models that support the quantitative and functional analysis of properties of Mircokernels.

SYANCO

bilateral DFG-NWO project "Synthesis and analysis of component connectors"

ProbPor II

One main goal of the DFG project "Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse II" was the implementation of the model checking tool LiQuor, which is designed for the analysis of reactive probabilistic systems against omega-regular linear-time specifications. Within this scope, research was also done on various theoretical foundations. Amongst others, a probabilistic variant of partial order reduction has been established and the minimization of automata for linear-time specifications has been investigated (see LTL2DSTAR).

ROCKS

The bilateral DFG/NWO project "Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems" focused on modelling and analysis techniques for large scale homogeneous and safety-critical heterogeneous systems.

PROCOPE

DAAD project PROCOPE: academic research collaboration with Dr. Nathalie Bertrand (France)

PROALAR

DAAD project PROALAR: academic research collaboration with Prof. Dr. Pedro D'Argenio (Argentina) (together with Prof. Dr. Holger Hermanns (Universität Saarbrücken))

CREDO

European Union project "Modeling and analysis of evolutionary structures for distributed services"

ProbPor

DFG-project "Reduktionsmethoden zur Verifikation omega-regulärer und temporallogischer Eigenschaften für kommunizierende probabilistische Prozesse"

VOSS I und VOSS II

The bilateral DFG/NWO-projects "Validation of Stochastic Systems I/II" aimed at the integration of modelling and computer-aided verification techniques for the analysis of complex systems with stochastic behaviour. Within the scope of the projects some prominent modelling and analysis techniques have been adapted and extended to a probabilistic setting and several new methods have been developed.

Veriam

DFG-project "Computerunterstützte Verifikation mit abstrakten Modellen"

DFG-Projekt MA 794/2-1 (und 2-2)

The topic of this project was action refinement in models of reactive systems.

DFG-Projekt MA 794/3-1 (und 3-2)

The topics of this project were specification formalism and the design of verification methods for probabilistic reactive systems.



Tools:

ProFeat

is a tool for feature-oriented modeling of families of probabilistic systems and their analysis using probabilistic model checking

LTL2DSTAR

a tool hat converts formulas in linear time logic to deterministic omega-automata, specifically Rabin and Streett automata

Vereofy

Component based model checking

JINC

an efficient, easy to use and easily expandable BDD package

Last modified: 20th Nov 2018, 10.43 AM
Author: Dr.-Ing. Sascha Klüppelholz

Contact
Prof. Dr.
Christel Baier

Phone: +49 (0) 351 463-38548
Fax: +49 (0) 351 463-38348
e-mail contact form