Support Unit: Computational Methods and Visualization

"Computational Methods and Visualization" supports climate policy advice with novel methods from theoretical and applied computer science. We develop and apply dependently typed domain-specific languages, verified methods for optimal control, visual analytics, visual data communication and climate services to understand, quantify and communicate the impact of uncertainties on climate policies that respect planetary boundaries and global viability constraints.

Motivation & Goals

Bridging the gap between climate science and policy advice requires an interdisciplinary effort and contributions from various disciplines: control and game theory, expert elicitation, agent-based modelling and simulation. Without languages that support formulating notions of accountability (of policies), safety (of operational spaces) or commitment in a precise, decidable way, this enterprise rests on shaky grounds. Theoretical computer science can bring significant contributions towards such languages. We develop small, embedded, dependently typed domain-specific languages for formulating and solving crucial questions on climate policy. These include the impact of unavoidable uncertainties (for example, due to the inertia of legislation) on optimal policies, the suitability of solar radiation management measures for mitigating the impacts of high greenhouse gas concentrations in the atmosphere and the formalization of notions of avoidability, commitment, responsibility and tipping behavior.

Within the visual analytics focus of our cross-cutting activity, we develop visualization solutions for Germany, Peru, Tanzania and India and execute surveys investigating the culture-dependent perception of climate visuals. Climate service solutions (e.g. for the financial sector) are developed, validated and improved. Moreover, we use computer vision and pattern recognition methods for the analysis of climate images and climate data.

Formal methods for climate policy advice

Type theory is a well established framework for modelling and for programming [1]: it is mature, with solid implementations (NuPRL, Coq, Agda, Idris, Lean), and impeccable mathematical credentials. It is also an ideal framework for developing computational theories [4], embedded domain-specific languages and verified methods [1,2].

Over the last decade and in collaboration with P. Jansson (Chalmers University of Technology, Gothenburg, Sweden), C. Ionescu (THD, Deggendorf, Germany and Oxford University, UK) and Tim Richter (University of Potsdam), we have developed a framework for the specification and the solution of finite horizon sequential decision problems under monadic uncertainty.

These problems are ubiquitous in climate research. They appear, for example, in integrated assessment models, in models of international environmental agreements and in stylized greenhouse gas emission (GHG) [3] and solar radiation management problems.

The framework supports, on the one hand, the formal specification of  policy targets, for example, mixing emission reductions and solar radiation management measures as to keep the climate end the economic systems within certain "safe" boundaries. On the other hand, it supports the computation of optimal policies. These are policies that provably (machine-checked) fulfill the targets under different kinds of uncertainty.

In collaboration with M. Crucifix (UCL, Louvain-la-Neuve, Belgium) and in the framework of the European TiPES (Tipping Points in the Earth System) project, we develop small domain specific languages for measuring the influence of decisions on GHG emissions and the suitability of solar radiation management measures for mitigating the impacts of climate change under tipping behavior uncertainty.

Visualization & Visual Analytics

Visualization is an established flexible tool to analyze climate related data and to communicate climate impact research findings to decision makers and the public. However, it faces multiple challenges:

• the heterogeneous characteristics of climate data sets [5],
• the multiple tasks to be performed [6], and
• the complexity of the climate science background.

We tackle these problems by making state-of-the-art visualization techniques and tools – including own developments – easy-to-use for scientists and other user groups such as teachers & pupils:

• visual analysis of ensemble climate simulations data / uncertainty visualization,
• climate network visualization [7], and
• climate and impact knowledge dissemination / web platforms (together with RD2)
• KlimafolgenOnline for Germany [8] (KlimafolgenOnline.com, ClimateImpactsOnline.com, KlimafolgenOnline-Bildung.de)
• the new KlimafolgenOnline prototype for developing countries (currently Tanzania and Peru): kfo.pik-potsdam.de, for a test account, please contact us at klimafolgen@pik-potsdam.de.

Sensitivity & Uncertainty

The complexity of the Earth system, the intrinsic variability of processes and our limited knowledge about the considered sub-systems demand a careful quality assurance of the findings from modeling studies. In particular, quantification of uncertainty and identification of sensitive processes, parameters or initial values are of continuous importance when studying climate (impact) phenomena by simulation models.

To support modelers and analysts we have developed the multi-run simulation environment SimEnv [11] mainly for sensitivity and uncertainty analyses of model output. Generic experiment types are based on probabilistic, deterministic and Bayesian sampling schemes in factor spaces and allow for flexible experimentation and later analyses.

Key Publications

1. Ionescu C., Jansson P., Botta N. (2018) Type Theory as a Framework for Modelling and Programming. In: Margaria T., Steffen B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Modeling. ISoLA 2018. Lecture Notes in Computer Science, vol 11244. Springer, Cham
2. N. Brede, N. Botta, Semantic verification of generic dynamic programming. in preparation.
3. N. Botta, P. Jansson, C. Ionescu. (2018) The impact of uncertainty on optimal emission policies. Earth Syst. Dynam., 9, 525-542, 2018.
4. Botta, N., Jansson, P. & Ionescu, C. (2017). Contributions to a computational theory of policy advice and avoidability. J. Funct. Program., 27, e23
5. H.-J. Schulz, T. Nocke, M. Heitzler, H. Schumann (2017) A Systematic View on Data Descriptors for the Visual Analysis of Tabular Data, Information Visualization, Vol. 16(3), 232-256.
6. H.-J. Schulz, T. Nocke, M. Heitzler, H. Schumann (2013) A design space of visualization tasks. IEEE Transactions on Visualization and Computer Graphics 19(12), 2366-2375, DOI: 10.1109/TVCG.2013.120, at IEEE InfoVis 2013.
7. T. Nocke, S. Buschmann, J.F. Donges, N. Marwan, H.-J. Schulz, C. Tominski (2015) Review: Visual analytics of climate networks, Nonlinear Processes in Geophysics, 22, 545-570.
8. I. Blumenthal, C. Schlenther, S. Hirsbrunner, M. Stock, T. Nocke (2018): Climate Impacts for German Schools—An Educational Web Portal Solution In: Leal Filho W. et al. (eds) Handbook of Climate Change Communication: Vol. 3. Case Studies in Climate Change Communication. Springer, 209-223.
9. B. Schneider, T. Nocke, G. Feulner (2014) Twist and Shout: Images and Graphs in Skeptical Climate Media, in B. Schneider and T. Nocke (eds.): Image Politics of Climate Change, Transcript Verlag, ISBN 978-3-8376-2610-0, pp. 153-186.
10. B. Schneider, T. Nocke (2017) The Feeling of Red and Blue—A Constructive Critique of Color Mapping in Visual Climate Change Communication In: Leal Filho W. et al. (eds) Handbook of Climate Change Communication: Vol. 2. Climate Change Management. Springer, 289-303.
11. M. Flechsig, U. Böhm, T. Nocke, C. Rachimow (2013) The multi-run simulation environment SimEnv. User’s Guide V3.1. PIK Potsdam, http://www.pik-potsdam.de/software/simenv

Projects