Abstract
The dynamic logic with binders D? was recently introduced as a suitable formalism to support a rigorous stepwise development method for reactive software. The commitment of this logic concerning bisimulation equivalence is, however, not satisfactory: the model class semantics of specifications in D? is not closed under bisimulation equivalence; there are D?-sentences that distinguish bisimulation equivalent models, i.e., D? does not enjoy the modal invariance property. This paper improves on these limitations by providing an observational semantics for dynamic logic with binders. This involves the definition of a new model category and of a more relaxed satisfaction relation. We show that the new logic D? ~ enjoys modal invariance and even the Hennessy-Milner property. Moreover, the new model category provides a categorical characterisation of bisimulation equivalence by observational isomorphism. Finally, we consider abstractor semantics obtained by closing the model class of a specification SP in D? under bisimulation equivalence. We show that, under mild conditions, abstractor semantics of SP in D? is the same as observational semantics of SP in D? ~.

Abstract

Abstract
This paper presents a computational framework for the optimization of maintenance activities for infrastructure assets, with particular emphasis being placed on road network assets. This framework incorporates degradation and maintenance models for infrastructure assets along with multi-objective optimization for searching optimal maintenance schedules. Given a schedule of maintenance actions, the future performance is estimated by means of a Monte Carlo simulation that enables to account for inherent uncertainties. The design variables of optimization are the types of maintenance actions and their timing over the planning horizon. The objectives are to minimize both the asset degradation and maintenance cost. This includes satisfaction of constraints representing performance demands. The proposed framework is general and can be applied to different types of infrastructure assets. The numerical results, obtained for a road bridge managed by a highway operating agency, demonstrate the validity and usefulness of the proposed framework.

Abstract
IEC 61850 is a communication standard for electrical Substation Automation Systems (SAS). It defines both the information model and services used for communication between Intelligent Electronic Devices (IEDs) in a substation. The adoption of this standard brings several advantages for the design and operation of substations. The abstract data models defined in IEC 61850 can be mapped upon application protocols, such as MMS, GOOSE or SMV. These protocols can run upon TCP/IP networks or upon specific high speed Ethernet LANs, in order to match the timing requirements associated to protective relaying mechanisms. For the specific case of GOOSE messages, the standard specifies the use of VLANs (Virtual LANs) with priority tagging (IEEE 802.1q) to implement separate virtual networks with the appropriate message priority levels, in order to ensure the specified response times. The lack of adequate simulation models that enable the response time assessment of both SMV and GOOSE messages is one of the shortcomings of available simulation tools. In this paper, we propose simulation models for the IEC 61850 communication standard, targeting application that use GOOSE and SMV messages. This simulation models has been built upon OMNeT++/INET. The simulation results obtained from a typical IEC 61850 communication scenario show the effectiveness of the developed models. Some of these results have been experimentally validated.

Abstract

Abstract
A great number of masonry arch bridges dates back to past centuries, being preserved by society due to their historical and still economic importance. Thereby, adequate preservation measures are required. Regarding masonry arch bridge's structural condition, it is relevant to consider its age, and consequently deterioration, and the fact that these bridges are submitted to loads higher than those for which they were conceived, being imperative to assess their structural performance. Regarding safety assessment requirements, there are different reliability levels, whose objectives are to analyse the ultimate load carrying capacity and the serviceability performance. This paper presents and discusses a framework that allows to determine the ultimate load-carrying capacity (Ultimate Limit State) of masonry arch bridges, using limit analysis and probabilistic approaches. Geometric and material data and load characterization, as well as inherent uncertainties will be also introduced. In order to determine the ultimate load-carrying capacity, the plastic theory will be employed, namely the limit analysis theorem, which is based on kinematic mechanisms. Since one of the main drawbacks of a probabilistic analysis is the required high computational resources, a sensitivity analysis is incorporated in order to reduce the analysis time. The presented framework is validated with an application to a set of existing Portuguese railway masonry arch bridges. (C) 2016 Published by Elsevier Ltd.