caa a22 4500 475797582 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20001201xx s 000 0 eng 10.1023/A:1026534200187 doi (NATIONALLICENCE)springer-10.1023/A:1026534200187 Logic Based Abstractions of Real-Time Systems [Elektronische Daten] [Roberto Barbuti, Nicoletta De Francesco, Antonella Santone, Gigiola Vaglini] When verifying concurrent systems described by transition systems, state explosion is one of the most serious problems. If quantitative temporal information (expressed by clock ticks) is considered, state explosion is even more serious. We present a notion of abstraction of transition systems, where the abstraction is driven by the formulae of a quantitative temporal logic, called qu-mu-calculus, defined in the paper. The abstraction is based on a notion of bisimulation equivalence, called 〈ρ, n〉-equivalence, where ρ is a set of actions and n is a natural number. It is proved that two transition systems are 〈ρ, n〉-equivalent iff they give the same truth value to all qu-mu-calculus formulae such that the actions occurring in the modal operators are contained in ρ, and with time constraints whose values are less than or equal to n. We present a non-standard (abstract) semantics for a timed process algebra able to produce reduced transition systems for checking formulae. The abstract semantics, parametric with respect to a set ρ of actions and a natural number n, produces a reduced transition system 〈ρ, n〉-equivalent to the standard one. A transformational method is also defined, by means of which it is possible to syntactically transform a program into a smaller one, still preserving 〈ρ, n〉-equivalence. Kluwer Academic Publishers, 2000 temporal logic nationallicence ATP nationallicence state explosion nationallicence Barbuti Roberto Dipartimento di Informatica, Università di Pisa, I-56125, Pisa, Italy aut De Francesco Nicoletta Dipartimento di Ingegneria dell'Informazione, Università di Pisa, I-56126, Pisa, Italy aut Santone Antonella Dipartimento di Ingegneria dell'Informazione, Università di Pisa, I-56126, Pisa, Italy aut Vaglini Gigiola Dipartimento di Ingegneria dell'Informazione, Università di Pisa, I-56126, Pisa, Italy aut Formal Methods in System Design Kluwer Academic Publishers 17/3(2000-12-01), 201-220 0925-9856 17:3<201 2000 17 10703 https://doi.org/10.1023/A:1026534200187 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1026534200187 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Barbuti Roberto Dipartimento di Informatica, Università di Pisa, I-56125, Pisa, Italy aut NATIONALLICENCE 700 1- De Francesco Nicoletta Dipartimento di Ingegneria dell'Informazione, Università di Pisa, I-56126, Pisa, Italy aut NATIONALLICENCE 700 1- Santone Antonella Dipartimento di Ingegneria dell'Informazione, Università di Pisa, I-56126, Pisa, Italy aut NATIONALLICENCE 700 1- Vaglini Gigiola Dipartimento di Ingegneria dell'Informazione, Università di Pisa, I-56126, Pisa, Italy aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 17/3(2000-12-01), 201-220 0925-9856 17:3<201 2000 17 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer