Search

Model checking timed automata becomes increasingly complex with the increase in the number of clocks. Hence it is desirable that one constructs an automaton with the minimum number of clocks possible. The problem of checking whether there exists a timed automaton with a smaller number of clocks such that the timed language accepted by the original automaton is preserved is known to be undecidable. In this paper, we give a construction, which for any given timed automaton produces a timed bisimilar automaton with the least number of clocks. Further, we show that such an automaton with the minimum possible number of clocks can be constructed in time that is doubly exponential in the number of clocks of the original automaton.

In this paper, we propose an at least as fast as relation between two timed automata states and investigate its decidability. The proposed relation is a prebisimulation and we show that given two processes with rational clock valuations it is decidable whether such a prebisimulation relation exists between them. Though bisimulation relations have been widely studied with respect to timed systems and timed automata, prebisimulations in timed systems form a much lesser studied area and according to our knowledge, this is the first of the kind where we study the decidability of a timed prebisimulation. This prebisimulation has been termed timed performance prebisimulation since it compares the efficiency of two states in terms of their performances in performing actions. if s and t are time abstracted bisimilar and every possible delay by s and its successors is no more than the delays performed by t and its successors where the delays are real numbers. The prebisimilarity defined here falls in between timed and time abstracted bisimilarity.

Software metrics are mainly utilized to measure and characterize the software development process. Cost, Time and Productivity are key attributes in the software development process. Predictability is the concept which leads to know prior the outcome of the system development. Predicting the various elements which relates to the software development process in advance is quite complex. The main aim of this paper is to propose a comprehensive set of software metrics for predicting the cost, time and productivity in advance with help of available inputs in the project instantiated. These metrics tends to be the horoscope of a project development. Our main objective is to resolve the complexity, enhancing the efficiency of the system development in earliest manner. This paper is mainly deals with analyzing and evaluating predictive metrics with predefined models. The implementation of the metrics to predict the outcome of the project whether the project leads to success or failure even before the project instantiated. If the project leads to success, predicting whether it attains massive or moderate profit. If the project leads to failure, check the alternative way to recover from failure i.e., to reduce the complexity and enhancement of efficiency.

Computed Tomography(CT) is extensively adopted in diagnostic imaging world over due to various advantages over other imaging techniques. This eventually resulted in higher population doses. Oman is also not an exception to this. In 2007, there is a fifteen percentage increase in CT examinations in Ministry of Health hospitals alone than the previous year. To obtain good quality CT scans with optimal patient dose, a comprehensive radiation acceptance and quality assurance programme has to be in place for CT scanners. Here in this study validation of such a programme employed in Ministry of Health, Oman for CT scanners in various Ministry of Health hospitals is discussed. Though a large number of parameters were analysed for the study, we include a few from them - Computer Tomography Dose Index (CTDI), Scatter radiation levels, CT numbers, Noise, Slice thickness from four different vendors.

We introduce a quantitative concept for bisimulations by integrating the notion of amortisation (cf. [3]). This allows us to make behavioural comparisons between nondeterministic systems that are inherently non-terminating and to analyse the relative long-term costs of deploying them. To this end, we conservatively extend CCS to include a new set of cost-based actions and define a cost-based quantitative relation called amortised bisimulation. We demonstrate the applicability of our approach by two case studies. In both cases the cost of additional administration is shown to amortise. We furthermore show that the amortised preorder for speed introduced in [6] is naturally expressible in our setting.

In this paper we present logical characterizations of two preorders, within the framework of Hennessy-Milner Logics. The two preorders (loosely termed bisimulation-based efficiency preorders) are on processes represented as labelled transition systems. The characterizations are particularly interesting as they explore preorders lying between strong and weak bisimilarity, guided by a principle of containment which is explained in the Introduction. Even though the proofs of the characterizations use standard methods, there are various subtleties introduced by the nature of the preorders and the logical operators needed to characterize them. The authors have not previously encountered the use of such operators in such simple logics.

In this paper a proof technique for reasoning about the multi-modal logic of beliefs and goals is defined based on resolution at different levels of a tree of clauses. We have considered belief and goal as normal modal logic operators. The technique is inspired by that in [6,7] and allows for a locality property to be satisfied. The main motivation for this work arises not as much from theorem-proving as from the notion of belief and goal revision under an assumption of consistency of the beliefs and goals of an agent. We also present proofs of soundness and completeness of the logic.

Multi-agent systems are receiving attention nowadays, as they can be applied in a variety of disciplines like industry, e-commerce, control systems, etc. As the areas of usage are more crucial the matter of assurance of correctness of programs is important. However, verification of these systems has received attention only very recently. Hitherto such systems have been programmed without a clearly defined formal semantics and with very little idea about formally expressed verifiable properties to be satisfied by such systems. In this paper a new multi-agent programming language, called ECCS is defined. Its operational semantics is defined and a model checking algorithm is described which verifies properties expressed in the logic ACTL.

Two notions for comparing the efficiencies of equivalent concurrent systems have been developed and axiomatized in [1] and [2]. Recently Natarajan and Cleaveland have defined a notion of testing [6] which incorporates these ideas as an extension of the testing methodology ([3],[4]). Their extension bounds the run of a test in an effort to compare processes for their relative efficiencies, measured in terms of the amount of internal activity in a process.

A simple efficiency preorder for CCS processes is introduced in which p≲q means that q is at least as fast as p, or more generally, p uses at least as much resources as q. It is shown to be preserved by all CCS contexts except summation and it is used to analyse a non-trivial example: two different implementations of a bounded buffer. Finally a sound and complete proof system for finite processes is given.