@article{UflackerKowarkZeier2011, author = {Uflacker, Matthias and Kowark, Thomas and Zeier, Alexander}, title = {An instrument for real-time design interaction capture}, isbn = {978-3-642-13756-3}, year = {2011}, language = {en} } @article{LuebbeWeske2011, author = {Luebbe, Alexander and Weske, Mathias}, title = {Bringing design thinking to business process modeling}, isbn = {978-3-642-13756-3}, year = {2011}, language = {en} } @article{HirschfeldSteinertLincke2011, author = {Hirschfeld, Robert and Steinert, Bastian and Lincke, Jens}, title = {Agile software development in virtual collaboration environments}, isbn = {978-3-642-13756-3}, year = {2011}, language = {en} } @article{GabrysiakGieseSeibel2011, author = {Gabrysiak, Gregor and Giese, Holger and Seibel, Andreas}, title = {Towards next generation design thinking : scenario-based prototyping for designing complex software systems with multiple users}, isbn = {978-3-642-13756-3}, year = {2011}, language = {en} } @article{HocherHeidenvonWebskyetal.2011, author = {Hocher, Berthold and Heiden, S. and von Websky, Karoline and Rahnenf{\"u}hrer, J{\"o}rg and Kalk, Philipp and Pfab, T.}, title = {Dual endothelin-converting enzyme/neutral endopeptidase blockade in rats with D-galactosamine-induced liver failure}, series = {European journal of medical research : official organ "Deutsche AIDS-Gesellschaft"}, volume = {16}, journal = {European journal of medical research : official organ "Deutsche AIDS-Gesellschaft"}, number = {6}, publisher = {Med. Scientific Publ. Holzapfel}, address = {M{\"u}nchen}, issn = {0949-2321}, pages = {275 -- 279}, year = {2011}, abstract = {Secondary activation of the endothelin system is thought to be involved in toxic liver injury. This study tested the hypothesis that dual endothelin-converting enzyme / neutral endopeptidase blockade might: be able to attenuate acute toxic liver injury. Male Sprague-Dawley rats were implanted with subcutaneous minipumps to deliver the novel compound SLV338 (10 mg/kg*d) or vehicle. Four days later they received two intraperitoneal injections of D-galactosamine (1.3 g/kg each) or vehicle at an interval of 12 hours. The animals were sacrificed 48 hours after the first injection. Injection of D-galactosamine resulted in very severe liver injury, reflected by strongly elevated plasma liver enzymes, hepatic necrosis and inflammation, and a mortality rate of 42.9 \%. SLV338 treatment did not show any significant effect on the extent of acute liver injury as judged from plasma parameters, hepatic histology and mortality. Plasma measurements of SLV338 confirmed adequate drug delivery. Plasma concentrations of big endothelin-1 and endothelin-1 were significantly elevated in animals with liver injury (5-fold and 62-fold, respectively). Plasma endothelin-1 was significantly correlated with several markers of liver injury. SLV338 completely prevented the rise of plasma big endothelin-1 (p<0.05) and markedly attenuated the rise of endothelin-1 (p = 0.055). In conclusion, dual endothelin-converting enzyme / neutral endopeptidase blockade by SLV338 did not significantly attenuate D-galactosamine-induced acute liver injury, although it largely prevented the activation of the endothelin system. An evaluation of SLV338 in a less severe model of liver injury would be of interest, since very severe intoxication might not be relevantly amenable to pharmacological interventions.}, language = {en} } @article{WeidlichMendlingWeske2011, author = {Weidlich, Matthias and Mendling, Jan and Weske, Mathias}, title = {Efficient consistency measurement based on behavioral profiles of process models}, series = {IEEE transactions on software engineering}, volume = {37}, journal = {IEEE transactions on software engineering}, number = {3}, publisher = {Inst. of Electr. and Electronics Engineers}, address = {Los Alamitos}, issn = {0098-5589}, doi = {10.1109/TSE.2010.96}, pages = {410 -- 429}, year = {2011}, abstract = {Engineering of process-driven business applications can be supported by process modeling efforts in order to bridge the gap between business requirements and system specifications. However, diverging purposes of business process modeling initiatives have led to significant problems in aligning related models at different abstract levels and different perspectives. Checking the consistency of such corresponding models is a major challenge for process modeling theory and practice. In this paper, we take the inappropriateness of existing strict notions of behavioral equivalence as a starting point. Our contribution is a concept called behavioral profile that captures the essential behavioral constraints of a process model. We show that these profiles can be computed efficiently, i.e., in cubic time for sound free-choice Petri nets w.r.t. their number of places and transitions. We use behavioral profiles for the definition of a formal notion of consistency which is less sensitive to model projections than common criteria of behavioral equivalence and allows for quantifying deviation in a metric way. The derivation of behavioral profiles and the calculation of a degree of consistency have been implemented to demonstrate the applicability of our approach. We also report the findings from checking consistency between partially overlapping models of the SAP reference model.}, language = {en} } @article{PolyvyanyyWeidlichWeske2011, author = {Polyvyanyy, Artem and Weidlich, Matthias and Weske, Mathias}, title = {Connectivity of workflow nets the foundations of stepwise verification}, series = {Acta informatica}, volume = {48}, journal = {Acta informatica}, number = {4}, publisher = {Springer}, address = {New York}, issn = {0001-5903}, doi = {10.1007/s00236-011-0137-8}, pages = {213 -- 242}, year = {2011}, abstract = {Behavioral models capture operational principles of real-world or designed systems. Formally, each behavioral model defines the state space of a system, i.e., its states and the principles of state transitions. Such a model is the basis for analysis of the system's properties. In practice, state spaces of systems are immense, which results in huge computational complexity for their analysis. Behavioral models are typically described as executable graphs, whose execution semantics encodes a state space. The structure theory of behavioral models studies the relations between the structure of a model and the properties of its state space. In this article, we use the connectivity property of graphs to achieve an efficient and extensive discovery of the compositional structure of behavioral models; behavioral models get stepwise decomposed into components with clear structural characteristics and inter-component relations. At each decomposition step, the discovered compositional structure of a model is used for reasoning on properties of the whole state space of the system. The approach is exemplified by means of a concrete behavioral model and verification criterion. That is, we analyze workflow nets, a well-established tool for modeling behavior of distributed systems, with respect to the soundness property, a basic correctness property of workflow nets. Stepwise verification allows the detection of violations of the soundness property by inspecting small portions of a model, thereby considerably reducing the amount of work to be done to perform soundness checks. Besides formal results, we also report on findings from applying our approach to an industry model collection.}, language = {en} } @article{JoergesMargariaSteffen2011, author = {J{\"o}rges, Sven and Margaria, Tiziana and Steffen, Bernhard}, title = {Assuring property conformance of code generators via model checking}, series = {Formal aspects of computing : the international journal of formal methods}, volume = {23}, journal = {Formal aspects of computing : the international journal of formal methods}, number = {5}, publisher = {Springer}, address = {New York}, issn = {0934-5043}, doi = {10.1007/s00165-010-0169-9}, pages = {589 -- 606}, year = {2011}, abstract = {Automatic code generation is an essential cornerstone of today's model-driven approaches to software engineering. Thus a key requirement for the success of this technique is the reliability and correctness of code generators. This article describes how we employ standard model checking-based verification to check that code generator models developed within our code generation framework Genesys conform to (temporal) properties. Genesys is a graphical framework for the high-level construction of code generators on the basis of an extensible library of well-defined building blocks along the lines of the Extreme Model-Driven Development paradigm. We will illustrate our verification approach by examining complex constraints for code generators, which even span entire model hierarchies. We also show how this leads to a knowledge base of rules for code generators, which we constantly extend by e.g. combining constraints to bigger constraints, or by deriving common patterns from structurally similar constraints. In our experience, the development of code generators with Genesys boils down to re-instantiating patterns or slightly modifying the graphical process model, activities which are strongly supported by verification facilities presented in this article.}, language = {en} } @article{RabenaltGoesselLeininger2011, author = {Rabenalt, Thomas and Goessel, Michael and Leininger, Andreas}, title = {Masking of X-Values by use of a hierarchically configurable register}, series = {Journal of electronic testing : theory and applications}, volume = {27}, journal = {Journal of electronic testing : theory and applications}, number = {1}, publisher = {Springer}, address = {Dordrecht}, issn = {0923-8174}, doi = {10.1007/s10836-010-5179-2}, pages = {31 -- 41}, year = {2011}, abstract = {In this paper we consider masking of unknowns (X-values) for VLSI circuits. We present a new hierarchical method of X-masking which is a major improvement of the method proposed in [4], called WIDE1. By the method proposed, the number of observable scan cells is optimized and data volume for X-masking can be significantly reduced in comparison to WIDEL This is demonstrated for three industrial designs. In cases where all X-values have to be masked the novel approach is especially efficient.}, language = {en} } @article{BordihnHolzerKutrib2011, author = {Bordihn, Henning and Holzer, Markus and Kutrib, Martin}, title = {Decidability of operation problems for TOL languages and subclasses}, series = {Information and computation}, volume = {209}, journal = {Information and computation}, number = {3}, publisher = {Elsevier}, address = {San Diego}, issn = {0890-5401}, doi = {10.1016/j.ic.2010.11.008}, pages = {344 -- 352}, year = {2011}, abstract = {We investigate the decidability of the operation problem for TOL languages and subclasses. Fix an operation on formal languages. Given languages from the family considered (OL languages, TOL languages, or their propagating variants), is the application of this operation to the given languages still a language that belongs to the same language family? Observe, that all the Lindenmayer language families in question are anti-AFLs, that is, they are not closed under homomorphisms, inverse homomorphisms, intersection with regular languages, union, concatenation, and Kleene closure. Besides these classical operations we also consider intersection and substitution, since the language families under consideration are not closed under these operations, too. We show that for all of the above mentioned language operations, except for the Kleene closure, the corresponding operation problems of OL and TOL languages and their propagating variants are not even semidecidable. The situation changes for unary OL languages. In this case we prove that the operation problems with respect to Kleene star, complementation, and intersection with regular sets are decidable.}, language = {en} } @article{CatchpolePlatzerWeikertetal.2011, author = {Catchpole, Gareth and Platzer, Alexander and Weikert, Cornelia and Kempkensteffen, Carsten and Johannsen, Manfred and Krause, Hans and Jung, Klaus and Miller, Kurt and Willmitzer, Lothar and Selbig, Joachim and Weikert, Steffen}, title = {Metabolic profiling reveals key metabolic features of renal cell carcinoma}, series = {Journal of cellular and molecular medicine : a journal of translational medicine}, volume = {15}, journal = {Journal of cellular and molecular medicine : a journal of translational medicine}, number = {1}, publisher = {Wiley-Blackwell}, address = {Malden}, issn = {1582-1838}, doi = {10.1111/j.1582-4934.2009.00939.x}, pages = {109 -- 118}, year = {2011}, abstract = {Recent evidence suggests that metabolic changes play a pivotal role in the biology of cancer and in particular renal cell carcinoma (RCC). Here, a global metabolite profiling approach was applied to characterize the metabolite pool of RCC and normal renal tissue. Advanced decision tree models were applied to characterize the metabolic signature of RCC and to explore features of metastasized tumours. The findings were validated in a second independent dataset. Vitamin E derivates and metabolites of glucose, fatty acid, and inositol phosphate metabolism determined the metabolic profile of RCC. alpha-tocopherol, hippuric acid, myoinositol, fructose-1-phosphate and glucose-1-phosphate contributed most to the tumour/normal discrimination and all showed pronounced concentration changes in RCC. The identified metabolic profile was characterized by a low recognition error of only 5\% for tumour versus normal samples. Data on metastasized tumours suggested a key role for metabolic pathways involving arachidonic acid, free fatty acids, proline, uracil and the tricarboxylic acid cycle. These results illustrate the potential of mass spectroscopy based metabolomics in conjunction with sophisticated data analysis methods to uncover the metabolic phenotype of cancer. Differentially regulated metabolites, such as vitamin E compounds, hippuric acid and myoinositol, provide leads for the characterization of novel pathways in RCC.}, language = {en} } @article{GebserLeeLierler2011, author = {Gebser, Martin and Lee, Joohyung and Lierler, Yuliya}, title = {On elementary loops of logic programs}, series = {Theory and practice of logic programming}, volume = {11}, journal = {Theory and practice of logic programming}, number = {2}, publisher = {Cambridge Univ. Press}, address = {New York}, issn = {1471-0684}, doi = {10.1017/S1471068411000019}, pages = {953 -- 988}, year = {2011}, abstract = {Using the notion of an elementary loop, Gebser and Schaub (2005. Proceedings of the Eighth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05), 53-65) refined the theorem on loop formulas attributable to Lin and Zhao (2004) by considering loop formulas of elementary loops only. In this paper, we reformulate the definition of an elementary loop, extend it to disjunctive programs, and study several properties of elementary loops, including how maximal elementary loops are related to minimal unfounded sets. The results provide useful insights into the stable model semantics in terms of elementary loops. For a nondisjunctive program, using a graph-theoretic characterization of an elementary loop, we show that the problem of recognizing an elementary loop is tractable. On the other hand, we also show that the corresponding problem is coNP-complete for a disjunctive program. Based on the notion of an elementary loop, we present the class of Head-Elementary-loop-Free (HEF) programs, which strictly generalizes the class of Head-Cycle-Free (HCF) programs attributable to Ben-Eliyahu and Dechter (1994. Annals of Mathematics and Artificial Intelligence 12, 53-87). Like an Ha: program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head atoms into the body.}, language = {en} } @article{BordihnKutribMalcher2011, author = {Bordihn, Henning and Kutrib, Martin and Malcher, Andreas}, title = {Undecidability and hierarchy results for parallel communicating finite automata}, series = {International journal of foundations of computer science}, volume = {22}, journal = {International journal of foundations of computer science}, number = {7}, publisher = {World Scientific}, address = {Singapore}, issn = {0129-0541}, doi = {10.1142/S0129054111008891}, pages = {1577 -- 1592}, year = {2011}, abstract = {Parallel communicating finite automata (PCFAs) are systems of several finite state automata which process a common input string in a parallel way and are able to communicate by sending their states upon request. We consider deterministic and nondeterministic variants and distinguish four working modes. It is known that these systems in the most general mode are as powerful as one-way multi-head finite automata. It is additionally known that the number of heads corresponds to the number of automata in PCFAs in a constructive way. Thus, undecidability results as well as results on the hierarchies induced by the number of heads carry over from multi-head finite automata to PCFAs in the most general mode. Here, we complement these undecidability and hierarchy results also for the remaining working modes. In particular, we show that classical decidability questions are not semi-decidable for any type of PCFAs under consideration. Moreover, it is proven that the number of automata in the system induces infinite hierarchies for deterministic and nondeterministic PCFAs in three working modes.}, language = {en} } @article{BakeraMargariaRenneretal.2011, author = {Bakera, Marco and Margaria, Tiziana and Renner, Clemens D. and Steffen, Bernhard}, title = {Game-Based model checking for reliable autonomy in space}, series = {Journal of aerospace computing, information, and communication}, volume = {8}, journal = {Journal of aerospace computing, information, and communication}, number = {4}, publisher = {American Institute of Aeronautics and Astronautics}, address = {Reston}, issn = {1940-3151}, doi = {10.2514/1.32013}, pages = {100 -- 114}, year = {2011}, abstract = {Autonomy is an emerging paradigm for the design and implementation of managed services and systems. Self-managed aspects frequently concern the communication of systems with their environment. Self-management subsystems are critical, they should thus be designed and implemented as high-assurance components. Here, we propose to use GEAR, a game-based model checker for the full modal mu-calculus, and derived, more user-oriented logics, as a user friendly tool that can offer automatic proofs of critical properties of such systems. Designers and engineers can interactively investigate automatically generated winning strategies resulting from the games, this way exploring the connection between the property, the system, and the proof. The benefits of the approach are illustrated on a case study that concerns the ExoMars Rover.}, language = {en} } @article{ArrighiNesmeWerner2011, author = {Arrighi, Pablo and Nesme, Vincent and Werner, Reinhard F.}, title = {One-Dimensional quantum cellular automata}, series = {International journal of unconventional computing : non-classical computation and cellular automata}, volume = {7}, journal = {International journal of unconventional computing : non-classical computation and cellular automata}, number = {4}, publisher = {Old City Publishing Science}, address = {Philadelphia}, issn = {1548-7199}, pages = {223 -- 244}, year = {2011}, abstract = {We define and study quantum cellular automata (QCA). We show that they are reversible and that the neighborhood of the inverse is the opposite of the neighborhood. We also show that QCA always admit, modulo shifts, a two-layered block representation. Note that the same two-layered block representation result applies also over infinite configurations, as was previously shown for one-dimensional systems in the more elaborate formalism of operators algebras [18]. Here the proof is simpler and self-contained, moreover we discuss a counterexample QCA in higher dimensions.}, language = {en} } @article{LindbergMeinelWagner2011, author = {Lindberg, Tilmann and Meinel, Christoph and Wagner, Ralf}, title = {Design thinking : a fruitful concept for IT development?}, isbn = {978-3-642-13756-3}, year = {2011}, language = {en} } @article{MeinelLeifer2011, author = {Meinel, Christoph and Leifer, Larry}, title = {Design thinking research}, isbn = {978-3-642-13756-3}, year = {2011}, language = {en} } @article{GumiennyMeinelGerickeetal.2011, author = {Gumienny, Raja and Meinel, Christoph and Gericke, Lutz and Quasthoff, Matthias and LoBue, Peter and Willems, Christian}, title = {Tele-board : enabling efficient collaboration in digital design spaces across time and distance}, isbn = {978-3-642-13756-3}, year = {2011}, language = {en} } @article{ThienenNoweskiMeineletal.2011, author = {Thienen, Julia von and Noweski, Christine and Meinel, Christoph and Rauth, Ingo}, title = {The co-evolution of theory and practice in design thinking - or - "Mind the oddness trap!"}, isbn = {978-3-642-13756-3}, year = {2011}, language = {en} } @article{ThonLandwehrDeRaedt2011, author = {Thon, Ingo and Landwehr, Niels and De Raedt, Luc}, title = {Stochastic relational processes efficient inference and applications}, series = {Machine learning}, volume = {82}, journal = {Machine learning}, number = {2}, publisher = {Springer}, address = {Dordrecht}, issn = {0885-6125}, doi = {10.1007/s10994-010-5213-8}, pages = {239 -- 272}, year = {2011}, abstract = {One of the goals of artificial intelligence is to develop agents that learn and act in complex environments. Realistic environments typically feature a variable number of objects, relations amongst them, and non-deterministic transition behavior. While standard probabilistic sequence models provide efficient inference and learning techniques for sequential data, they typically cannot fully capture the relational complexity. On the other hand, statistical relational learning techniques are often too inefficient to cope with complex sequential data. In this paper, we introduce a simple model that occupies an intermediate position in this expressiveness/efficiency trade-off. It is based on CP-logic (Causal Probabilistic Logic), an expressive probabilistic logic for modeling causality. However, by specializing CP-logic to represent a probability distribution over sequences of relational state descriptions and employing a Markov assumption, inference and learning become more tractable and effective. Specifically, we show how to solve part of the inference and learning problems directly at the first-order level, while transforming the remaining part into the problem of computing all satisfying assignments for a Boolean formula in a binary decision diagram. We experimentally validate that the resulting technique is able to handle probabilistic relational domains with a substantial number of objects and relations.}, language = {en} }