We present a logic for stating properties such as, “after a request for service there is at least a 98% probability that the service will be carried out within 2 seconds”. The logic extends the temporal logic CTL by Emerson, Clarke and Sistla with time and probabilities. Formulas are interpreted over discrete time Markov chains. We give algorithms for checking that a given Markov chain satisfies a formula in the logic. The algorithms require a polynomial number of arithmetic operations, in size of both the formula and the Markov chain. A simple example is included to illustrate the algorithms.

A process algebra that extends R. Milner's (1983) calculus of communicating systems (CCS) with probabilities and time is presented. With this calculus it is possible to describe real-time and reliability aspects of distributed systems. A (strong) bisimulation equivalence is defined, and a corresponding complete axiomatization is given. Several examples are included.

This paper presents a state-of-practice (SOP) overview of automotive communication technologies, including the latest technology developments. These networking tech- nologies are classied in four major groups: (1) current wired, (2) multimedia, (3) upcoming wired and (4) wire- less. Within these groups a few technologies stand out as strong candidates for future automotive networks. The goal of this paper is to give an overview of automotive applica- tions relying on communications, identify the key network- ing technologies used in various automotive applications, present their properties and attributes, and indicate future challenges in the area of automotive communications.