Technical and economic factors in applying the enhanced coalbed methane recovery process

Geological sequestration of CO2 is a technically feasible and potentially economic option for significantly and safely reducing greenhouse gas emissions, with CO2 injection already practiced in Canada and the USA to enhance crude oil production. The Enhanced Coalbed Methane (ECBM) process is seen as the next most economical sequestration options. The authors estimate an incremental methane recovery factor from 20% to 50%, depending on coal rank and seam depth. Others have estimated the potential to increase worldwide CBM production, utilising ECBM, by 18 Trillion cubic meters, while simultaneously sequestering 345 Giga tonnes of CO2. This paper presents technical and economic factors to consider for developing a commercial ECBM project. Technical factors include: geostructural and hydrogeological issues, geochemical reactions, stressed and competitive sorption, counter-diffusion, effective and relative 4-D coal permeability and methane recovery levels. Key economic factors are injectant acquisition price, sale price of methane and the level of carbon credits.

Compositional class refinement in object-Z

Object-Z allows coupling constraints between classes which, on the one hand, facilitate specification at a high level of abstraction, but, on the other hand, make class refinement non-compositional. The consequence of this is that refinement is not practical for large Systems. This paper overcomes this limitation by introducing a methodology for compositional class refinement in Object-Z. The key step is an equivalence transformation of an arbitrary Object-Z specification to one in which introduced constraints prohibit non-compositional refinements. The methodology also allows the constraints which couple classes to be refined yielding an unrestricted approach to compositional class refinement.

Continuous action system refinement

Action systems are a framework for reasoning about discrete reactive systems. Back, Petre and Porres have extended these action systems to continuous action systems, which can be. used to model hybrid systems. In this paper we define a refinement relation, and develop practical data refinement rules for continuous action systems. The meaning of continuous action systems is expressed in terms of a mapping from continuous action systems to action systems. First, we present a new mapping from continuous act ion systems to action systems, such that Back's definition of trace refinement is correct with respect to it. Second, we present a stream semantics that is compatible with the trace semantics, but is preferable to it because it is more general. Although action system trace refinement rules are applicable to continuous action systems with a stream semantics, they are not complete. Finally, we introduce a new data refinement rule that is valid with respect to the stream semantics and can be used to prove refinements that are not possible in the trace semantics, and we analyse the completeness of our new rule in conjunction with the existing trace refinement rules.

Reasoning algebraically about probabilistic loops

Back and von Wright have developed algebraic laws for reasoning about loops in the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems. In particular we focus on developing data refinement rules for probabilistic action systems. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible. In particular, our probabilistic action system data refinement rules are new.