TY - JOUR A1 - Weidlich, Matthias A1 - Mendling, Jan A1 - Weske, Mathias T1 - Efficient consistency measurement based on behavioral profiles of process models JF - IEEE transactions on software engineering N2 - 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. KW - Process model analysis KW - process model alignment KW - behavioral abstraction KW - consistency checking KW - consistency measures Y1 - 2011 U6 - https://doi.org/10.1109/TSE.2010.96 SN - 0098-5589 VL - 37 IS - 3 SP - 410 EP - 429 PB - Inst. of Electr. and Electronics Engineers CY - Los Alamitos ER - TY - JOUR A1 - Uflacker, Matthias A1 - Kowark, Thomas A1 - Zeier, Alexander T1 - An instrument for real-time design interaction capture Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Thon, Ingo A1 - Landwehr, Niels A1 - De Raedt, Luc T1 - Stochastic relational processes efficient inference and applications JF - Machine learning N2 - 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. KW - Statistical relational learning KW - Stochastic relational process KW - Markov processes KW - Time series KW - CP-Logic Y1 - 2011 U6 - https://doi.org/10.1007/s10994-010-5213-8 SN - 0885-6125 VL - 82 IS - 2 SP - 239 EP - 272 PB - Springer CY - Dordrecht ER - TY - JOUR A1 - Thienen, Julia von A1 - Noweski, Christine A1 - Meinel, Christoph A1 - Rauth, Ingo T1 - The co-evolution of theory and practice in design thinking - or - "Mind the oddness trap!" Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Rabenalt, Thomas A1 - Goessel, Michael A1 - Leininger, Andreas T1 - Masking of X-Values by use of a hierarchically configurable register JF - Journal of electronic testing : theory and applications N2 - 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. KW - Masking of X-values KW - Hierarchically configurable mask register Y1 - 2011 U6 - https://doi.org/10.1007/s10836-010-5179-2 SN - 0923-8174 VL - 27 IS - 1 SP - 31 EP - 41 PB - Springer CY - Dordrecht ER - TY - JOUR A1 - Polyvyanyy, Artem A1 - Weidlich, Matthias A1 - Weske, Mathias T1 - Connectivity of workflow nets the foundations of stepwise verification JF - Acta informatica N2 - 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. Y1 - 2011 U6 - https://doi.org/10.1007/s00236-011-0137-8 SN - 0001-5903 VL - 48 IS - 4 SP - 213 EP - 242 PB - Springer CY - New York ER - TY - JOUR A1 - Mileo, Alessandra A1 - Schaub, Torsten H. A1 - Merico, Davide A1 - Bisiani, Roberto T1 - Knowledge-based multi-criteria optimization to support indoor positioning JF - Annals of mathematics and artificial intelligence N2 - Indoor position estimation constitutes a central task in home-based assisted living environments. Such environments often rely on a heterogeneous collection of low-cost sensors whose diversity and lack of precision has to be compensated by advanced techniques for localization and tracking. Although there are well established quantitative methods in robotics and neighboring fields for addressing these problems, they lack advanced knowledge representation and reasoning capacities. Such capabilities are not only useful in dealing with heterogeneous and incomplete information but moreover they allow for a better inclusion of semantic information and more general homecare and patient-related knowledge. We address this problem and investigate how state-of-the-art localization and tracking methods can be combined with Answer Set Programming, as a popular knowledge representation and reasoning formalism. We report upon a case-study and provide a first experimental evaluation of knowledge-based position estimation both in a simulated as well as in a real setting. KW - Knowledge representation KW - Answer Set Programming KW - Wireless Sensor Networks KW - Localization KW - Tracking Y1 - 2011 U6 - https://doi.org/10.1007/s10472-011-9241-2 SN - 1012-2443 SN - 1573-7470 VL - 62 IS - 3-4 SP - 345 EP - 370 PB - Springer CY - Dordrecht ER - TY - JOUR A1 - Meinel, Christoph A1 - Leifer, Larry T1 - Design thinking research Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Luebbe, Alexander A1 - Weske, Mathias T1 - Bringing design thinking to business process modeling Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Lindberg, Tilmann A1 - Meinel, Christoph A1 - Wagner, Ralf T1 - Design thinking : a fruitful concept for IT development? Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Jörges, Sven A1 - Margaria, Tiziana A1 - Steffen, Bernhard T1 - Assuring property conformance of code generators via model checking JF - Formal aspects of computing : the international journal of formal methods N2 - 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. KW - Extreme Model-Driven Development KW - Code generation KW - Model checking KW - Verification Y1 - 2011 U6 - https://doi.org/10.1007/s00165-010-0169-9 SN - 0934-5043 VL - 23 IS - 5 SP - 589 EP - 606 PB - Springer CY - New York ER - TY - JOUR A1 - Hocher, Berthold A1 - Heiden, S. A1 - von Websky, Karoline A1 - Rahnenführer, Jörg A1 - Kalk, Philipp A1 - Pfab, T. T1 - Dual endothelin-converting enzyme/neutral endopeptidase blockade in rats with D-galactosamine-induced liver failure JF - European journal of medical research : official organ "Deutsche AIDS-Gesellschaft" N2 - 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. KW - endothelin KW - endothelin-converting enzyme KW - neutral endopeptidase KW - D-galactosamine KW - acute liver failure Y1 - 2011 SN - 0949-2321 VL - 16 IS - 6 SP - 275 EP - 279 PB - Med. Scientific Publ. Holzapfel CY - München ER - TY - JOUR A1 - Hirschfeld, Robert A1 - Steinert, Bastian A1 - Lincke, Jens T1 - Agile software development in virtual collaboration environments Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Gumienny, Raja A1 - Meinel, Christoph A1 - Gericke, Lutz A1 - Quasthoff, Matthias A1 - LoBue, Peter A1 - Willems, Christian T1 - Tele-board : enabling efficient collaboration in digital design spaces across time and distance Y1 - 2011 SN - 978-3-642-13756-3 ER - TY - JOUR A1 - Gebser, Martin A1 - Schaub, Torsten H. A1 - Thiele, Sven A1 - Veber, Philippe T1 - Detecting inconsistencies in large biological networks with answer set programming JF - Theory and practice of logic programming N2 - We introduce an approach to detecting inconsistencies in large biological networks by using answer set programming. To this end, we build upon a recently proposed notion of consistency between biochemical/genetic reactions and high-throughput profiles of cell activity. We then present an approach based on answer set programming to check the consistency of large-scale data sets. Moreover, we extend this methodology to provide explanations for inconsistencies by determining minimal representations of conflicts. In practice, this can be used to identify unreliable data or to indicate missing reactions. KW - answer set programming KW - bioinformatics KW - consistency KW - diagnosis Y1 - 2011 U6 - https://doi.org/10.1017/S1471068410000554 SN - 1471-0684 VL - 11 IS - 5-6 SP - 323 EP - 360 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Gebser, Martin A1 - Sabuncu, Orkunt A1 - Schaub, Torsten H. T1 - An incremental answer set programming based system for finite model computation JF - AI communications : AICOM ; the European journal on artificial intelligence N2 - We address the problem of Finite Model Computation (FMC) of first-order theories and show that FMC can efficiently and transparently be solved by taking advantage of a recent extension of Answer Set Programming (ASP), called incremental Answer Set Programming (iASP). The idea is to use the incremental parameter in iASP programs to account for the domain size of a model. The FMC problem is then successively addressed for increasing domain sizes until an answer set, representing a finite model of the original first-order theory, is found. We implemented a system based on the iASP solver iClingo and demonstrate its competitiveness by showing that it slightly outperforms the winner of the FNT division of CADE's 2009 Automated Theorem Proving (ATP) competition on the respective benchmark collection. KW - Incremental answer set programming KW - finite model computation Y1 - 2011 U6 - https://doi.org/10.3233/AIC-2011-0496 SN - 0921-7126 VL - 24 IS - 2 SP - 195 EP - 212 PB - IOS Press CY - Amsterdam ER - TY - JOUR A1 - Gebser, Martin A1 - Lee, Joohyung A1 - Lierler, Yuliya T1 - On elementary loops of logic programs JF - Theory and practice of logic programming N2 - 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. KW - stable model semantics KW - loop formulas KW - unfounded sets Y1 - 2011 U6 - https://doi.org/10.1017/S1471068411000019 SN - 1471-0684 VL - 11 IS - 2 SP - 953 EP - 988 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Gebser, Martin A1 - Kaufmann, Benjamin A1 - Kaminski, Roland A1 - Ostrowski, Max A1 - Schaub, Torsten H. A1 - Schneider, Marius T1 - Potassco the Potsdam answer set solving collection JF - AI communications : AICOM ; the European journal on artificial intelligence N2 - This paper gives an overview of the open source project Potassco, the Potsdam Answer Set Solving Collection, bundling tools for Answer Set Programming developed at the University of Potsdam. KW - Answer set programming KW - declarative problem solving Y1 - 2011 U6 - https://doi.org/10.3233/AIC-2011-0491 SN - 0921-7126 VL - 24 IS - 2 SP - 107 EP - 124 PB - IOS Press CY - Amsterdam ER - TY - JOUR A1 - Gebser, Martin A1 - Kaminski, Roland A1 - Schaub, Torsten H. T1 - Complex optimization in answer set programming JF - Theory and practice of logic programming N2 - Preference handling and optimization are indispensable means for addressing nontrivial applications in Answer Set Programming (ASP). However, their implementation becomes difficult whenever they bring about a significant increase in computational complexity. As a consequence, existing ASP systems do not offer complex optimization capacities, supporting, for instance, inclusion-based minimization or Pareto efficiency. Rather, such complex criteria are typically addressed by resorting to dedicated modeling techniques, like saturation. Unlike the ease of common ASP modeling, however, these techniques are rather involved and hardly usable by ASP laymen. We address this problem by developing a general implementation technique by means of meta-prpogramming, thus reusing existing ASP systems to capture various forms of qualitative preferences among answer sets. In this way, complex preferences and optimization capacities become readily available for ASP applications. KW - Answer Set Programming KW - Preference Handling KW - Complex optimization KW - Meta-Programming Y1 - 2011 U6 - https://doi.org/10.1017/S1471068411000329 SN - 1471-0684 VL - 11 IS - 3 SP - 821 EP - 839 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Gabrysiak, Gregor A1 - Giese, Holger A1 - Seibel, Andreas T1 - Towards next generation design thinking : scenario-based prototyping for designing complex software systems with multiple users Y1 - 2011 SN - 978-3-642-13756-3 ER -